Theorem iuneq1 4958

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-v 3438  df-ss 3920  df-iun 4943

This theorem is referenced by:  iuneq1d  4969  iinvdif  5029  iunxprg  5045  iununi  5048  iunsuc  6394  funopsn  7082  funiunfv  7184  onfununi  8264  iunfi  9233  ttrclselem1  9621  ttrclselem2  9622  rankuni2b  9749  pwsdompw  10097  ackbij1lem7  10119  r1om  10137  fictb  10138  cfsmolem  10164  ituniiun  10316  domtriomlem  10336  domtriom  10337  inar1  10669  fsum2d  15678  fsumiun  15728  ackbijnn  15735  fprod2d  15888  prmreclem5  16832  lpival  21231  fiuncmp  23289  ovolfiniun  25400  ovoliunnul  25406  finiunmbl  25443  volfiniun  25446  voliunlem1  25449  iuninc  32504  ofpreima2  32609  gsumpart  33010  esum2dlem  34059  sigaclfu2  34088  sigapildsyslem  34128  fiunelros  34141  bnj548  34864  bnj554  34866  bnj594  34879  neibastop2lem  36334  istotbnd3  37751  0totbnd  37753  sstotbnd2  37754  sstotbnd  37755  sstotbnd3  37756  totbndbnd  37769  prdstotbnd  37774  cntotbnd  37776  heibor  37801  dfrcl4  43649  iunrelexp0  43675  comptiunov2i  43679  corclrcl  43680  cotrcltrcl  43698  trclfvdecomr  43701  dfrtrcl4  43711  corcltrcl  43712  cotrclrcl  43715  fiiuncl  45043  sge0iunmptlemfi  46394  caragenfiiuncl  46496  carageniuncllem1  46502  ovnsubadd2lem  46626