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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ⊆ wss 3913  ∪ ciun 4959

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rex 3070  df-v 3448  df-in 3920  df-ss 3930  df-iun 4961

This theorem is referenced by:  iuneq1d  4986  iinvdif  5045  iunxprg  5061  iununi  5064  iunsuc  6407  funopsn  7099  funiunfv  7200  onfununi  8292  iunfi  9291  ttrclselem1  9670  ttrclselem2  9671  rankuni2b  9798  pwsdompw  10149  ackbij1lem7  10171  r1om  10189  fictb  10190  cfsmolem  10215  ituniiun  10367  domtriomlem  10387  domtriom  10388  inar1  10720  fsum2d  15667  fsumiun  15717  ackbijnn  15724  fprod2d  15875  prmreclem5  16803  lpival  20774  fiuncmp  22792  ovolfiniun  24902  ovoliunnul  24908  finiunmbl  24945  volfiniun  24948  voliunlem1  24951  iuninc  31546  ofpreima2  31649  gsumpart  31967  esum2dlem  32780  sigaclfu2  32809  sigapildsyslem  32849  fiunelros  32862  bnj548  33598  bnj554  33600  bnj594  33613  neibastop2lem  34908  istotbnd3  36303  0totbnd  36305  sstotbnd2  36306  sstotbnd  36307  sstotbnd3  36308  totbndbnd  36321  prdstotbnd  36326  cntotbnd  36328  heibor  36353  dfrcl4  42070  iunrelexp0  42096  comptiunov2i  42100  corclrcl  42101  cotrcltrcl  42119  trclfvdecomr  42122  dfrtrcl4  42132  corcltrcl  42133  cotrclrcl  42136  fiiuncl  43395  iuneq1i  43417  sge0iunmptlemfi  44774  caragenfiiuncl  44876  carageniuncllem1  44882  ovnsubadd2lem  45006