Theorem iuneq2dv 4905

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∪ ciun 4881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3443  df-in 3888  df-ss 3898  df-iun 4883

This theorem is referenced by:  iuneq12d  4909  iuneq2d  4910  fparlem3  7792  fparlem4  7793  oalim  8140  omlim  8141  oelim  8142  oelim2  8204  r1val3  9251  imasdsval  16780  acsfn  16922  tgidm  21585  cmpsub  22005  alexsublem  22649  bcth3  23935  ovoliunlem1  24106  voliunlem1  24154  uniiccdif  24182  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem4  24190  itg2monolem1  24354  taylpfval  24960  ofpreima2  30429  fnpreimac  30434  esum2dlem  31461  eulerpartlemgu  31745  cvmscld  32633  satom  32716  msubvrs  32920  mblfinlem2  35095  ftc1anclem6  35135  heibor  35259  prjspval2  39607  trclfvcom  40424  scottrankd  40956  meaiininclem  43125  carageniuncllem2  43161  hoidmv1le  43233  hoidmvle  43239  ovnhoilem2  43241  ovnhoi  43242  ovnlecvr2  43249  ovncvr2  43250  hspmbl  43268  ovolval4lem1  43288  ovnovollem1  43295  ovnovollem2  43296  iunhoiioo  43315  vonioolem2  43320  smflimlem4  43407  smflimlem6  43409