Theorem iuneq1 5007

Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998.)

Assertion

Ref	Expression
iuneq1	⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐶(𝑥)

Proof of Theorem iuneq1

Step	Hyp	Ref	Expression
1		iunss1 5005	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)
2		iunss1 5005	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
3	1, 2	anim12i 612	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
4		eqss 3993	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3993	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 ↔ (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1534   ⊆ wss 3944  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rex 3066  df-v 3471  df-in 3951  df-ss 3961  df-iun 4993

This theorem is referenced by:  iuneq1d  5018  iinvdif  5077  iunxprg  5093  iununi  5096  iunsuc  6448  funopsn  7151  funiunfv  7252  onfununi  8355  iunfi  9356  ttrclselem1  9740  ttrclselem2  9741  rankuni2b  9868  pwsdompw  10219  ackbij1lem7  10241  r1om  10259  fictb  10260  cfsmolem  10285  ituniiun  10437  domtriomlem  10457  domtriom  10458  inar1  10790  fsum2d  15741  fsumiun  15791  ackbijnn  15798  fprod2d  15949  prmreclem5  16880  lpival  21203  fiuncmp  23295  ovolfiniun  25417  ovoliunnul  25423  finiunmbl  25460  volfiniun  25463  voliunlem1  25466  iuninc  32336  ofpreima2  32435  gsumpart  32747  esum2dlem  33647  sigaclfu2  33676  sigapildsyslem  33716  fiunelros  33729  bnj548  34464  bnj554  34466  bnj594  34479  neibastop2lem  35780  istotbnd3  37179  0totbnd  37181  sstotbnd2  37182  sstotbnd  37183  sstotbnd3  37184  totbndbnd  37197  prdstotbnd  37202  cntotbnd  37204  heibor  37229  dfrcl4  43029  iunrelexp0  43055  comptiunov2i  43059  corclrcl  43060  cotrcltrcl  43078  trclfvdecomr  43081  dfrtrcl4  43091  corcltrcl  43092  cotrclrcl  43095  fiiuncl  44352  iuneq1i  44374  sge0iunmptlemfi  45724  caragenfiiuncl  45826  carageniuncllem1  45832  ovnsubadd2lem  45956