Theorem iuneq1 4984

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-v 3461  df-ss 3943  df-iun 4969

This theorem is referenced by:  iuneq1d  4995  iinvdif  5056  iunxprg  5072  iununi  5075  iunsuc  6439  funopsn  7138  funiunfv  7240  onfununi  8355  iunfi  9355  ttrclselem1  9739  ttrclselem2  9740  rankuni2b  9867  pwsdompw  10217  ackbij1lem7  10239  r1om  10257  fictb  10258  cfsmolem  10284  ituniiun  10436  domtriomlem  10456  domtriom  10457  inar1  10789  fsum2d  15787  fsumiun  15837  ackbijnn  15844  fprod2d  15997  prmreclem5  16940  lpival  21285  fiuncmp  23342  ovolfiniun  25454  ovoliunnul  25460  finiunmbl  25497  volfiniun  25500  voliunlem1  25503  iuninc  32541  ofpreima2  32644  gsumpart  33051  esum2dlem  34123  sigaclfu2  34152  sigapildsyslem  34192  fiunelros  34205  bnj548  34928  bnj554  34930  bnj594  34943  neibastop2lem  36378  istotbnd3  37795  0totbnd  37797  sstotbnd2  37798  sstotbnd  37799  sstotbnd3  37800  totbndbnd  37813  prdstotbnd  37818  cntotbnd  37820  heibor  37845  dfrcl4  43700  iunrelexp0  43726  comptiunov2i  43730  corclrcl  43731  cotrcltrcl  43749  trclfvdecomr  43752  dfrtrcl4  43762  corcltrcl  43763  cotrclrcl  43766  fiiuncl  45089  sge0iunmptlemfi  46442  caragenfiiuncl  46544  carageniuncllem1  46550  ovnsubadd2lem  46674