Theorem iuneq1 4961

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ⊆ wss 3899  ∪ ciun 4944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-v 3440  df-ss 3916  df-iun 4946

This theorem is referenced by:  iuneq1d  4972  iinvdif  5033  iunxprg  5049  iununi  5052  iunsuc  6402  funopsn  7091  funiunfv  7192  onfununi  8271  iunfi  9241  ttrclselem1  9632  ttrclselem2  9633  rankuni2b  9763  pwsdompw  10111  ackbij1lem7  10133  r1om  10151  fictb  10152  cfsmolem  10178  ituniiun  10330  domtriomlem  10350  domtriom  10351  inar1  10684  fsum2d  15692  fsumiun  15742  ackbijnn  15749  fprod2d  15902  prmreclem5  16846  lpival  21277  fiuncmp  23346  ovolfiniun  25456  ovoliunnul  25462  finiunmbl  25499  volfiniun  25502  voliunlem1  25505  iuninc  32584  ofpreima2  32693  gsumpart  33095  esum2dlem  34198  sigaclfu2  34227  sigapildsyslem  34267  fiunelros  34280  bnj548  35002  bnj554  35004  bnj594  35017  neibastop2lem  36503  istotbnd3  37911  0totbnd  37913  sstotbnd2  37914  sstotbnd  37915  sstotbnd3  37916  totbndbnd  37929  prdstotbnd  37934  cntotbnd  37936  heibor  37961  dfrcl4  43859  iunrelexp0  43885  comptiunov2i  43889  corclrcl  43890  cotrcltrcl  43908  trclfvdecomr  43911  dfrtrcl4  43921  corcltrcl  43922  cotrclrcl  43925  fiiuncl  45252  sge0iunmptlemfi  46599  caragenfiiuncl  46701  carageniuncllem1  46707  ovnsubadd2lem  46831