Theorem iuneq1 4967

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ⊆ wss 3896  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-v 3452  df-ss 3897  df-iun 4952

This theorem is used by:  iuneq1d  4978  iinvdif  5039  iunxprg  5055  iununi  5058  iunopeqop  5494  iunsuc  6453  funopsn  7156  funopsnOLD  7157  funiunfv  7256  onfununi  8356  iunfi  9339  ttrclselem1  9733  ttrclselem2  9734  rankuni2b  9874  pwsdompw  10288  ackbij1lem7  10310  hfom  10328  fictb  10329  cfsmolem  10355  ituniiun  10507  domtriomlem  10527  domtriom  10528  inar1  10867  fsum2d  15946  fsumiun  15997  ackbijnn  16006  fprod2d  16157  prmreclem5  17107  lpival  21657  fiuncmp  23731  ovolfiniun  25831  ovoliunnul  25837  finiunmbl  25874  volfiniun  25877  voliunlem1  25880  iuninc  33206  ofpreima2  33311  gsumpart  33674  esum2dlem  34774  sigaclfu2  34803  sigapildsyslem  34844  fiunelros  34857  bnj548  35577  bnj554  35579  bnj594  35592  neibastop2lem  37244  ttceq  37372  istotbnd3  38814  0totbnd  38816  sstotbnd2  38817  sstotbnd  38818  sstotbnd3  38819  totbndbnd  38832  prdstotbnd  38837  cntotbnd  38839  heibor  38864  dfrcl4  44785  iunrelexp0  44811  comptiunov2i  44815  corclrcl  44816  cotrcltrcl  44834  trclfvdecomr  44837  dfrtrcl4  44847  corcltrcl  44848  cotrclrcl  44851  fiiuncl  46190  sge0iunmptlemfi  47531  caragenfiiuncl  47633  carageniuncllem1  47639  ovnsubadd2lem  47763