Theorem iuneq2dv 4973

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

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

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 3444  df-ss 3920  df-iun 4950

This theorem is referenced by:  iuneq12dOLD  4977  iuneq12d  4978  iuneq2d  4979  fparlem3  8066  fparlem4  8067  oalim  8469  omlim  8470  oelim  8471  oelim2  8533  r1val3  9762  imasdsval  17448  acsfn  17594  tgidm  22936  cmpsub  23356  alexsublem  24000  bcth3  25299  ovoliunlem1  25471  voliunlem1  25519  uniiccdif  25547  uniioombllem2  25552  uniioombllem3a  25553  uniioombllem4  25555  itg2monolem1  25719  taylpfval  26340  dmdju  32737  ofpreima2  32756  fnpreimac  32760  ssdifidllem  33549  esum2dlem  34270  eulerpartlemgu  34555  cvmscld  35489  satom  35572  msubvrs  35776  mblfinlem2  37909  ftc1anclem6  37949  heibor  38072  prjspval2  42971  trclfvcom  44079  scottrankd  44604  meaiininclem  46844  carageniuncllem2  46880  hoidmv1le  46952  hoidmvle  46958  ovnhoilem2  46960  ovnhoi  46961  ovnlecvr2  46968  ovncvr2  46969  hspmbl  46987  ovolval4lem1  47007  ovnovollem1  47014  ovnovollem2  47015  iunhoiioo  47034  vonioolem2  47039  smflimlem4  47132  smflimlem6  47134