Theorem iuneq2dv 4959

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∪ ciun 4934

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3432  df-ss 3907  df-iun 4936

This theorem is referenced by:  iuneq12dOLD  4963  iuneq12d  4964  iuneq2d  4965  fparlem3  8058  fparlem4  8059  oalim  8461  omlim  8462  oelim  8463  oelim2  8525  r1val3  9756  imasdsval  17473  acsfn  17619  tgidm  22958  cmpsub  23378  alexsublem  24022  bcth3  25311  ovoliunlem1  25482  voliunlem1  25530  uniiccdif  25558  uniioombllem2  25563  uniioombllem3a  25564  uniioombllem4  25566  itg2monolem1  25730  taylpfval  26344  dmdju  32738  ofpreima2  32757  fnpreimac  32761  ssdifidllem  33534  esum2dlem  34255  eulerpartlemgu  34540  cvmscld  35474  satom  35557  msubvrs  35761  mblfinlem2  37996  ftc1anclem6  38036  heibor  38159  prjspval2  43063  trclfvcom  44171  scottrankd  44696  meaiininclem  46935  carageniuncllem2  46971  hoidmv1le  47043  hoidmvle  47049  ovnhoilem2  47051  ovnhoi  47052  ovnlecvr2  47059  ovncvr2  47060  hspmbl  47078  ovolval4lem1  47098  ovnovollem1  47105  ovnovollem2  47106  iunhoiioo  47125  vonioolem2  47130  smflimlem4  47223  smflimlem6  47225