Theorem iuneq1 4968

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

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

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 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  iuneq1d  4979  iinvdif  5039  iunxprg  5055  iununi  5058  iunsuc  6407  funopsn  7102  funiunfv  7204  onfununi  8287  iunfi  9270  ttrclselem1  9654  ttrclselem2  9655  rankuni2b  9782  pwsdompw  10132  ackbij1lem7  10154  r1om  10172  fictb  10173  cfsmolem  10199  ituniiun  10351  domtriomlem  10371  domtriom  10372  inar1  10704  fsum2d  15713  fsumiun  15763  ackbijnn  15770  fprod2d  15923  prmreclem5  16867  lpival  21210  fiuncmp  23267  ovolfiniun  25378  ovoliunnul  25384  finiunmbl  25421  volfiniun  25424  voliunlem1  25427  iuninc  32462  ofpreima2  32563  gsumpart  32970  esum2dlem  34055  sigaclfu2  34084  sigapildsyslem  34124  fiunelros  34137  bnj548  34860  bnj554  34862  bnj594  34875  neibastop2lem  36321  istotbnd3  37738  0totbnd  37740  sstotbnd2  37741  sstotbnd  37742  sstotbnd3  37743  totbndbnd  37756  prdstotbnd  37761  cntotbnd  37763  heibor  37788  dfrcl4  43638  iunrelexp0  43664  comptiunov2i  43668  corclrcl  43669  cotrcltrcl  43687  trclfvdecomr  43690  dfrtrcl4  43700  corcltrcl  43701  cotrclrcl  43704  fiiuncl  45032  sge0iunmptlemfi  46384  caragenfiiuncl  46486  carageniuncllem1  46492  ovnsubadd2lem  46616