Theorem iuneq1 4947

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1539   ⊆ wss 3892  ∪ ciun 4931

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rex 3072  df-v 3439  df-in 3899  df-ss 3909  df-iun 4933

This theorem is referenced by:  iuneq1d  4958  iinvdif  5016  iunxprg  5032  iununi  5035  iunsuc  6365  funopsn  7052  funiunfv  7153  onfununi  8203  iunfi  9151  ttrclselem1  9527  ttrclselem2  9528  rankuni2b  9655  pwsdompw  10006  ackbij1lem7  10028  r1om  10046  fictb  10047  cfsmolem  10072  ituniiun  10224  domtriomlem  10244  domtriom  10245  inar1  10577  fsum2d  15528  fsumiun  15578  ackbijnn  15585  fprod2d  15736  prmreclem5  16666  lpival  20561  fiuncmp  22600  ovolfiniun  24710  ovoliunnul  24716  finiunmbl  24753  volfiniun  24756  voliunlem1  24759  iuninc  30945  ofpreima2  31048  gsumpart  31360  esum2dlem  32105  sigaclfu2  32134  sigapildsyslem  32174  fiunelros  32187  bnj548  32922  bnj554  32924  bnj594  32937  neibastop2lem  34594  istotbnd3  35973  0totbnd  35975  sstotbnd2  35976  sstotbnd  35977  sstotbnd3  35978  totbndbnd  35991  prdstotbnd  35996  cntotbnd  35998  heibor  36023  dfrcl4  41322  iunrelexp0  41348  comptiunov2i  41352  corclrcl  41353  cotrcltrcl  41371  trclfvdecomr  41374  dfrtrcl4  41384  corcltrcl  41385  cotrclrcl  41388  fiiuncl  42651  iuneq1i  42673  sge0iunmptlemfi  44001  caragenfiiuncl  44103  carageniuncllem1  44109  ovnsubadd2lem  44233