Theorem iuneq2dv 4981

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 3158	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐶)
3		iuneq2 4976	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 = 𝐶 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)
4	2, 3	syl 18	1 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∀wral 3080  ∪ ciun 4956

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-ss 3901  df-iun 4958

This theorem is used by:  iuneq12d  4985  iuneq2d  4986  fparlem3  8162  fparlem4  8163  oalim  8578  omlim  8579  oelim  8580  oelim2  8642  r1val3  9887  scottrankd  9986  imasdsval  17737  acsfn  17883  ssdifidllem  21691  tgidm  23353  cmpsub  23773  alexsublem  24418  bcth3  25707  ovoliunlem1  25878  voliunlem1  25926  uniiccdif  25954  uniioombllem2  25959  uniioombllem3a  25960  uniioombllem4  25962  itg2monolem1  26126  taylpfval  26749  dmdju  33339  ofpreima2  33358  fnpreimac  33362  esum2dlem  34835  eulerpartlemgu  35120  cvmscld  36246  satom  36329  msubvrs  36533  mblfinlem2  38844  ftc1anclem6  38884  heibor  39021  prjspval2  43907  trclfvcom  44984  meaiininclem  47769  carageniuncllem2  47805  hoidmv1le  47877  hoidmvle  47883  ovnhoilem2  47885  ovnhoi  47886  ovnlecvr2  47893  ovncvr2  47894  hspmbl  47912  ovolval4lem1  47932  ovnovollem1  47939  ovnovollem2  47940  iunhoiioo  47959  vonioolem2  47964  smflimlem4  48057  smflimlem6  48059