Theorem iuneq1 4956

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3897  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-v 3438  df-ss 3914  df-iun 4941

This theorem is referenced by:  iuneq1d  4967  iinvdif  5026  iunxprg  5042  iununi  5045  iunsuc  6393  funopsn  7081  funiunfv  7182  onfununi  8261  iunfi  9227  ttrclselem1  9615  ttrclselem2  9616  rankuni2b  9746  pwsdompw  10094  ackbij1lem7  10116  r1om  10134  fictb  10135  cfsmolem  10161  ituniiun  10313  domtriomlem  10333  domtriom  10334  inar1  10666  fsum2d  15678  fsumiun  15728  ackbijnn  15735  fprod2d  15888  prmreclem5  16832  lpival  21261  fiuncmp  23319  ovolfiniun  25429  ovoliunnul  25435  finiunmbl  25472  volfiniun  25475  voliunlem1  25478  iuninc  32540  ofpreima2  32648  gsumpart  33037  esum2dlem  34105  sigaclfu2  34134  sigapildsyslem  34174  fiunelros  34187  bnj548  34909  bnj554  34911  bnj594  34924  neibastop2lem  36402  istotbnd3  37819  0totbnd  37821  sstotbnd2  37822  sstotbnd  37823  sstotbnd3  37824  totbndbnd  37837  prdstotbnd  37842  cntotbnd  37844  heibor  37869  dfrcl4  43717  iunrelexp0  43743  comptiunov2i  43747  corclrcl  43748  cotrcltrcl  43766  trclfvdecomr  43769  dfrtrcl4  43779  corcltrcl  43780  cotrclrcl  43783  fiiuncl  45110  sge0iunmptlemfi  46459  caragenfiiuncl  46561  carageniuncllem1  46567  ovnsubadd2lem  46691