Theorem iuneq1 5031

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ⊆ wss 3976  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-v 3490  df-ss 3993  df-iun 5017

This theorem is referenced by:  iuneq1d  5042  iinvdif  5103  iunxprg  5119  iununi  5122  iunsuc  6480  funopsn  7182  funiunfv  7285  onfununi  8397  iunfi  9411  ttrclselem1  9794  ttrclselem2  9795  rankuni2b  9922  pwsdompw  10272  ackbij1lem7  10294  r1om  10312  fictb  10313  cfsmolem  10339  ituniiun  10491  domtriomlem  10511  domtriom  10512  inar1  10844  fsum2d  15819  fsumiun  15869  ackbijnn  15876  fprod2d  16029  prmreclem5  16967  lpival  21357  fiuncmp  23433  ovolfiniun  25555  ovoliunnul  25561  finiunmbl  25598  volfiniun  25601  voliunlem1  25604  iuninc  32583  ofpreima2  32684  gsumpart  33038  esum2dlem  34056  sigaclfu2  34085  sigapildsyslem  34125  fiunelros  34138  bnj548  34873  bnj554  34875  bnj594  34888  neibastop2lem  36326  istotbnd3  37731  0totbnd  37733  sstotbnd2  37734  sstotbnd  37735  sstotbnd3  37736  totbndbnd  37749  prdstotbnd  37754  cntotbnd  37756  heibor  37781  dfrcl4  43638  iunrelexp0  43664  comptiunov2i  43668  corclrcl  43669  cotrcltrcl  43687  trclfvdecomr  43690  dfrtrcl4  43700  corcltrcl  43701  cotrclrcl  43704  fiiuncl  44967  sge0iunmptlemfi  46334  caragenfiiuncl  46436  carageniuncllem1  46442  ovnsubadd2lem  46566