Theorem iuneq1 4975

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-v 3452  df-ss 3934  df-iun 4960

This theorem is referenced by:  iuneq1d  4986  iinvdif  5047  iunxprg  5063  iununi  5066  iunsuc  6422  funopsn  7123  funiunfv  7225  onfununi  8313  iunfi  9301  ttrclselem1  9685  ttrclselem2  9686  rankuni2b  9813  pwsdompw  10163  ackbij1lem7  10185  r1om  10203  fictb  10204  cfsmolem  10230  ituniiun  10382  domtriomlem  10402  domtriom  10403  inar1  10735  fsum2d  15744  fsumiun  15794  ackbijnn  15801  fprod2d  15954  prmreclem5  16898  lpival  21241  fiuncmp  23298  ovolfiniun  25409  ovoliunnul  25415  finiunmbl  25452  volfiniun  25455  voliunlem1  25458  iuninc  32496  ofpreima2  32597  gsumpart  33004  esum2dlem  34089  sigaclfu2  34118  sigapildsyslem  34158  fiunelros  34171  bnj548  34894  bnj554  34896  bnj594  34909  neibastop2lem  36355  istotbnd3  37772  0totbnd  37774  sstotbnd2  37775  sstotbnd  37776  sstotbnd3  37777  totbndbnd  37790  prdstotbnd  37795  cntotbnd  37797  heibor  37822  dfrcl4  43672  iunrelexp0  43698  comptiunov2i  43702  corclrcl  43703  cotrcltrcl  43721  trclfvdecomr  43724  dfrtrcl4  43734  corcltrcl  43735  cotrclrcl  43738  fiiuncl  45066  sge0iunmptlemfi  46418  caragenfiiuncl  46520  carageniuncllem1  46526  ovnsubadd2lem  46650