Theorem iuneq1 4945

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3891  ∪ ciun 4929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3432  df-in 3898  df-ss 3908  df-iun 4931

This theorem is referenced by:  iuneq1d  4956  iinvdif  5013  iunxprg  5029  iununi  5032  iunsuc  6345  funopsn  7014  funiunfv  7115  onfununi  8156  iunfi  9068  ttrclselem1  9444  ttrclselem2  9445  trpredlem1  9457  trpredtr  9460  trpredmintr  9461  trpredrec  9467  rankuni2b  9595  pwsdompw  9944  ackbij1lem7  9966  r1om  9984  fictb  9985  cfsmolem  10010  ituniiun  10162  domtriomlem  10182  domtriom  10183  inar1  10515  fsum2d  15464  fsumiun  15514  ackbijnn  15521  fprod2d  15672  prmreclem5  16602  lpival  20497  fiuncmp  22536  ovolfiniun  24646  ovoliunnul  24652  finiunmbl  24689  volfiniun  24692  voliunlem1  24695  iuninc  30879  ofpreima2  30982  gsumpart  31294  esum2dlem  32039  sigaclfu2  32068  sigapildsyslem  32108  fiunelros  32121  bnj548  32856  bnj554  32858  bnj594  32871  neibastop2lem  34528  istotbnd3  35908  0totbnd  35910  sstotbnd2  35911  sstotbnd  35912  sstotbnd3  35913  totbndbnd  35926  prdstotbnd  35931  cntotbnd  35933  heibor  35958  dfrcl4  41237  iunrelexp0  41263  comptiunov2i  41267  corclrcl  41268  cotrcltrcl  41286  trclfvdecomr  41289  dfrtrcl4  41299  corcltrcl  41300  cotrclrcl  41303  fiiuncl  42566  iuneq1i  42588  sge0iunmptlemfi  43905  caragenfiiuncl  44007  carageniuncllem1  44013  ovnsubadd2lem  44137