Theorem iuneq1 4961

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1541   ⊆ wss 3901  ∪ ciun 4945

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 2708

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-rex 3072  df-v 3444  df-in 3908  df-ss 3918  df-iun 4947

This theorem is referenced by:  iuneq1d  4972  iinvdif  5031  iunxprg  5047  iununi  5050  iunsuc  6390  funopsn  7080  funiunfv  7181  onfununi  8246  iunfi  9209  ttrclselem1  9586  ttrclselem2  9587  rankuni2b  9714  pwsdompw  10065  ackbij1lem7  10087  r1om  10105  fictb  10106  cfsmolem  10131  ituniiun  10283  domtriomlem  10303  domtriom  10304  inar1  10636  fsum2d  15582  fsumiun  15632  ackbijnn  15639  fprod2d  15790  prmreclem5  16718  lpival  20621  fiuncmp  22660  ovolfiniun  24770  ovoliunnul  24776  finiunmbl  24813  volfiniun  24816  voliunlem1  24819  iuninc  31185  ofpreima2  31288  gsumpart  31600  esum2dlem  32356  sigaclfu2  32385  sigapildsyslem  32425  fiunelros  32438  bnj548  33174  bnj554  33176  bnj594  33189  neibastop2lem  34686  istotbnd3  36085  0totbnd  36087  sstotbnd2  36088  sstotbnd  36089  sstotbnd3  36090  totbndbnd  36103  prdstotbnd  36108  cntotbnd  36110  heibor  36135  dfrcl4  41657  iunrelexp0  41683  comptiunov2i  41687  corclrcl  41688  cotrcltrcl  41706  trclfvdecomr  41709  dfrtrcl4  41719  corcltrcl  41720  cotrclrcl  41723  fiiuncl  42985  iuneq1i  43007  sge0iunmptlemfi  44340  caragenfiiuncl  44442  carageniuncllem1  44448  ovnsubadd2lem  44572