Theorem iuneq2dv 4976

Description: Equality deduction for indexed union. (Contributed by NM, 3-Aug-2004.)

Hypothesis

Ref	Expression
iuneq2dv.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
iuneq2dv	⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem iuneq2dv

Step	Hyp	Ref	Expression
1		iuneq2dv.1	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
2	1	ralrimiva 3155	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4971	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 18	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077  ∪ ciun 4951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-v 3453  df-ss 3916  df-iun 4953

This theorem is used by:  iuneq12d  4980  iuneq2d  4981  fparlem3  8125  fparlem4  8126  oalim  8540  omlim  8541  oelim  8542  oelim2  8604  r1val3  9850  scottrankd  9949  imasdsval  17687  acsfn  17833  ssdifidllem  21640  tgidm  23298  cmpsub  23718  alexsublem  24363  bcth3  25652  ovoliunlem1  25823  voliunlem1  25871  uniiccdif  25899  uniioombllem2  25904  uniioombllem3a  25905  uniioombllem4  25907  itg2monolem1  26071  taylpfval  26692  dmdju  33241  ofpreima2  33260  fnpreimac  33264  esum2dlem  34724  eulerpartlemgu  35009  cvmscld  36038  satom  36121  msubvrs  36325  mblfinlem2  38576  ftc1anclem6  38616  heibor  38755  prjspval2  43641  trclfvcom  44722  meaiininclem  47495  carageniuncllem2  47531  hoidmv1le  47603  hoidmvle  47609  ovnhoilem2  47611  ovnhoi  47612  ovnlecvr2  47619  ovncvr2  47620  hspmbl  47638  ovolval4lem1  47658  ovnovollem1  47665  ovnovollem2  47666  iunhoiioo  47685  vonioolem2  47690  smflimlem4  47783  smflimlem6  47785