Theorem iuneq1 4973

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4958

This theorem is used by:  iuneq1d  4984  iinvdif  5045  iunxprg  5061  iununi  5064  iunopeqop  5501  iunsuc  6476  funopsn  7183  funopsnOLD  7184  funiunfv  7283  onfununi  8387  iunfi  9370  ttrclselem1  9763  ttrclselem2  9764  rankuni2b  9904  pwsdompw  10320  ackbij1lem7  10342  hfom  10360  fictb  10361  cfsmolem  10387  ituniiun  10539  domtriomlem  10559  domtriom  10560  inar1  10899  fsum2d  15981  fsumiun  16032  ackbijnn  16041  fprod2d  16192  prmreclem5  17142  lpival  21699  fiuncmp  23777  ovolfiniun  25877  ovoliunnul  25883  finiunmbl  25920  volfiniun  25923  voliunlem1  25926  iuninc  33253  ofpreima2  33358  gsumpart  33723  esum2dlem  34835  sigaclfu2  34864  sigapildsyslem  34905  fiunelros  34918  bnj548  35638  bnj554  35640  bnj594  35653  neibastop2lem  37363  ttceq  37491  istotbnd3  38971  0totbnd  38973  sstotbnd2  38974  sstotbnd  38975  sstotbnd3  38976  totbndbnd  38989  prdstotbnd  38994  cntotbnd  38996  heibor  39021  dfrcl4  44937  iunrelexp0  44963  comptiunov2i  44967  corclrcl  44968  cotrcltrcl  44986  trclfvdecomr  44989  dfrtrcl4  44999  corcltrcl  45000  cotrclrcl  45003  ackbij3  46289  fiiuncl  46356  sge0iunmptlemfi  47696  caragenfiiuncl  47798  carageniuncllem1  47804  ovnsubadd2lem  47928