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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  ∀wral 3079  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-v 3457  df-ss 3922  df-iun 4958

This theorem is referenced by:  iuneq12dOLD  4985  iuneq12d  4986  iuneq2d  4987  fparlem3  8105  fparlem4  8106  oalim  8513  omlim  8514  oelim  8515  oelim2  8577  r1val3  9806  scottrankd  9870  imasdsval  17564  acsfn  17710  ssdifidllem  21484  tgidm  23137  cmpsub  23557  alexsublem  24201  bcth3  25490  ovoliunlem1  25661  voliunlem1  25709  uniiccdif  25737  uniioombllem2  25742  uniioombllem3a  25743  uniioombllem4  25745  itg2monolem1  25909  taylpfval  26528  dmdju  32992  ofpreima2  33011  fnpreimac  33015  esum2dlem  34482  eulerpartlemgu  34767  cvmscld  35765  satom  35848  msubvrs  36052  mblfinlem2  38329  ftc1anclem6  38369  heibor  38492  prjspval2  43365  trclfvcom  44469  meaiininclem  47220  carageniuncllem2  47256  hoidmv1le  47328  hoidmvle  47334  ovnhoilem2  47336  ovnhoi  47337  ovnlecvr2  47344  ovncvr2  47345  hspmbl  47363  ovolval4lem1  47383  ovnovollem1  47390  ovnovollem2  47391  iunhoiioo  47410  vonioolem2  47415  smflimlem4  47508  smflimlem6  47510