Theorem iuneq1 4972

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 4970	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶)
2		iunss1 4970	. . 3 ⊢ (𝐵 ⊆ 𝐴 → ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶)
3	1, 2	anim12i 613	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
4		eqss 3962	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
5		eqss 3962	. 2 ⊢ (∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶 ↔ (∪ 𝑥 ∈ 𝐴 𝐶 ⊆ ∪ 𝑥 ∈ 𝐵 𝐶 ∧ ∪ 𝑥 ∈ 𝐵 𝐶 ⊆ ∪ 𝑥 ∈ 𝐴 𝐶))
6	3, 4, 5	3imtr4i 292	1 ⊢ (𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ⊆ wss 3914  ∪ ciun 4955

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3449  df-ss 3931  df-iun 4957

This theorem is referenced by:  iuneq1d  4983  iinvdif  5044  iunxprg  5060  iununi  5063  iunsuc  6419  funopsn  7120  funiunfv  7222  onfununi  8310  iunfi  9294  ttrclselem1  9678  ttrclselem2  9679  rankuni2b  9806  pwsdompw  10156  ackbij1lem7  10178  r1om  10196  fictb  10197  cfsmolem  10223  ituniiun  10375  domtriomlem  10395  domtriom  10396  inar1  10728  fsum2d  15737  fsumiun  15787  ackbijnn  15794  fprod2d  15947  prmreclem5  16891  lpival  21234  fiuncmp  23291  ovolfiniun  25402  ovoliunnul  25408  finiunmbl  25445  volfiniun  25448  voliunlem1  25451  iuninc  32489  ofpreima2  32590  gsumpart  32997  esum2dlem  34082  sigaclfu2  34111  sigapildsyslem  34151  fiunelros  34164  bnj548  34887  bnj554  34889  bnj594  34902  neibastop2lem  36348  istotbnd3  37765  0totbnd  37767  sstotbnd2  37768  sstotbnd  37769  sstotbnd3  37770  totbndbnd  37783  prdstotbnd  37788  cntotbnd  37790  heibor  37815  dfrcl4  43665  iunrelexp0  43691  comptiunov2i  43695  corclrcl  43696  cotrcltrcl  43714  trclfvdecomr  43717  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731  fiiuncl  45059  sge0iunmptlemfi  46411  caragenfiiuncl  46513  carageniuncllem1  46519  ovnsubadd2lem  46643