Theorem iuneq1 4965

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ⊆ wss 3903  ∪ ciun 4948

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-v 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  iuneq1d  4976  iinvdif  5037  iunxprg  5053  iununi  5056  iunsuc  6412  funopsn  7103  funiunfv  7204  onfununi  8283  iunfi  9255  ttrclselem1  9646  ttrclselem2  9647  rankuni2b  9777  pwsdompw  10125  ackbij1lem7  10147  r1om  10165  fictb  10166  cfsmolem  10192  ituniiun  10344  domtriomlem  10364  domtriom  10365  inar1  10698  fsum2d  15706  fsumiun  15756  ackbijnn  15763  fprod2d  15916  prmreclem5  16860  lpival  21291  fiuncmp  23360  ovolfiniun  25470  ovoliunnul  25476  finiunmbl  25513  volfiniun  25516  voliunlem1  25519  iuninc  32647  ofpreima2  32756  gsumpart  33157  esum2dlem  34270  sigaclfu2  34299  sigapildsyslem  34339  fiunelros  34352  bnj548  35073  bnj554  35075  bnj594  35088  neibastop2lem  36576  istotbnd3  38022  0totbnd  38024  sstotbnd2  38025  sstotbnd  38026  sstotbnd3  38027  totbndbnd  38040  prdstotbnd  38045  cntotbnd  38047  heibor  38072  dfrcl4  44032  iunrelexp0  44058  comptiunov2i  44062  corclrcl  44063  cotrcltrcl  44081  trclfvdecomr  44084  dfrtrcl4  44094  corcltrcl  44095  cotrclrcl  44098  fiiuncl  45425  sge0iunmptlemfi  46771  caragenfiiuncl  46873  carageniuncllem1  46879  ovnsubadd2lem  47003