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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ∪ 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-ral 3045  df-rex 3054  df-v 3446  df-ss 3928  df-iun 4953

This theorem is referenced by:  iuneq12dOLD  4980  iuneq12d  4981  iuneq2d  4982  fparlem3  8070  fparlem4  8071  oalim  8473  omlim  8474  oelim  8475  oelim2  8536  r1val3  9767  imasdsval  17454  acsfn  17600  tgidm  22900  cmpsub  23320  alexsublem  23964  bcth3  25264  ovoliunlem1  25436  voliunlem1  25484  uniiccdif  25512  uniioombllem2  25517  uniioombllem3a  25518  uniioombllem4  25520  itg2monolem1  25684  taylpfval  26305  dmdju  32621  ofpreima2  32640  fnpreimac  32645  ssdifidllem  33420  esum2dlem  34075  eulerpartlemgu  34361  cvmscld  35253  satom  35336  msubvrs  35540  mblfinlem2  37645  ftc1anclem6  37685  heibor  37808  prjspval2  42594  trclfvcom  43705  scottrankd  44230  meaiininclem  46477  carageniuncllem2  46513  hoidmv1le  46585  hoidmvle  46591  ovnhoilem2  46593  ovnhoi  46594  ovnlecvr2  46601  ovncvr2  46602  hspmbl  46620  ovolval4lem1  46640  ovnovollem1  46647  ovnovollem2  46648  iunhoiioo  46667  vonioolem2  46672  smflimlem4  46765  smflimlem6  46767