Theorem iuneq1 4971

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3902  ∪ ciun 4954

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3089  df-v 3455  df-ss 3919  df-iun 4956

This theorem is used by:  iuneq1d  4982  iinvdif  5044  iunxprg  5060  iununi  5063  iunopeqop  5502  iunsuc  6449  funopsn  7148  funopsnOLD  7149  funiunfv  7249  onfununi  8334  iunfi  9314  ttrclselem1  9708  ttrclselem2  9709  rankuni2b  9839  pwsdompw  10209  ackbij1lem7  10231  r1om  10249  fictb  10250  cfsmolem  10276  ituniiun  10428  domtriomlem  10448  domtriom  10449  inar1  10788  fsum2d  15861  fsumiun  15912  ackbijnn  15921  fprod2d  16074  prmreclem5  17018  lpival  21561  fiuncmp  23635  ovolfiniun  25735  ovoliunnul  25741  finiunmbl  25778  volfiniun  25781  voliunlem1  25784  iuninc  33042  ofpreima2  33147  gsumpart  33511  esum2dlem  34610  sigaclfu2  34639  sigapildsyslem  34680  fiunelros  34693  bnj548  35414  bnj554  35416  bnj594  35429  neibastop2lem  36987  ttceq  37115  istotbnd3  38529  0totbnd  38531  sstotbnd2  38532  sstotbnd  38533  sstotbnd3  38534  totbndbnd  38547  prdstotbnd  38552  cntotbnd  38554  heibor  38579  dfrcl4  44524  iunrelexp0  44550  comptiunov2i  44554  corclrcl  44555  cotrcltrcl  44573  trclfvdecomr  44576  dfrtrcl4  44586  corcltrcl  44587  cotrclrcl  44590  fiiuncl  45907  sge0iunmptlemfi  47249  caragenfiiuncl  47351  carageniuncllem1  47357  ovnsubadd2lem  47481