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  21266  fiuncmp  23324  ovolfiniun  25435  ovoliunnul  25441  finiunmbl  25478  volfiniun  25481  voliunlem1  25484  iuninc  32539  ofpreima2  32640  gsumpart  33040  esum2dlem  34075  sigaclfu2  34104  sigapildsyslem  34144  fiunelros  34157  bnj548  34880  bnj554  34882  bnj594  34895  neibastop2lem  36341  istotbnd3  37758  0totbnd  37760  sstotbnd2  37761  sstotbnd  37762  sstotbnd3  37763  totbndbnd  37776  prdstotbnd  37781  cntotbnd  37783  heibor  37808  dfrcl4  43658  iunrelexp0  43684  comptiunov2i  43688  corclrcl  43689  cotrcltrcl  43707  trclfvdecomr  43710  dfrtrcl4  43720  corcltrcl  43721  cotrclrcl  43724  fiiuncl  45052  sge0iunmptlemfi  46404  caragenfiiuncl  46506  carageniuncllem1  46512  ovnsubadd2lem  46636