Theorem iuneq2dv 4971

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  ∀wral 3051  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-v 3442  df-ss 3918  df-iun 4948

This theorem is referenced by:  iuneq12dOLD  4975  iuneq12d  4976  iuneq2d  4977  fparlem3  8056  fparlem4  8057  oalim  8459  omlim  8460  oelim  8461  oelim2  8523  r1val3  9750  imasdsval  17436  acsfn  17582  tgidm  22924  cmpsub  23344  alexsublem  23988  bcth3  25287  ovoliunlem1  25459  voliunlem1  25507  uniiccdif  25535  uniioombllem2  25540  uniioombllem3a  25541  uniioombllem4  25543  itg2monolem1  25707  taylpfval  26328  dmdju  32725  ofpreima2  32744  fnpreimac  32749  ssdifidllem  33537  esum2dlem  34249  eulerpartlemgu  34534  cvmscld  35467  satom  35550  msubvrs  35754  mblfinlem2  37859  ftc1anclem6  37899  heibor  38022  prjspval2  42866  trclfvcom  43974  scottrankd  44499  meaiininclem  46740  carageniuncllem2  46776  hoidmv1le  46848  hoidmvle  46854  ovnhoilem2  46856  ovnhoi  46857  ovnlecvr2  46864  ovncvr2  46865  hspmbl  46883  ovolval4lem1  46903  ovnovollem1  46910  ovnovollem2  46911  iunhoiioo  46930  vonioolem2  46935  smflimlem4  47028  smflimlem6  47030