Theorem iuneq2dv 4992

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051  ∪ ciun 4967

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-v 3461  df-ss 3943  df-iun 4969

This theorem is referenced by:  iuneq12dOLD  4996  iuneq12d  4997  iuneq2d  4998  fparlem3  8113  fparlem4  8114  oalim  8544  omlim  8545  oelim  8546  oelim2  8607  r1val3  9852  imasdsval  17529  acsfn  17671  tgidm  22918  cmpsub  23338  alexsublem  23982  bcth3  25283  ovoliunlem1  25455  voliunlem1  25503  uniiccdif  25531  uniioombllem2  25536  uniioombllem3a  25537  uniioombllem4  25539  itg2monolem1  25703  taylpfval  26324  dmdju  32625  ofpreima2  32644  fnpreimac  32649  ssdifidllem  33471  esum2dlem  34123  eulerpartlemgu  34409  cvmscld  35295  satom  35378  msubvrs  35582  mblfinlem2  37682  ftc1anclem6  37722  heibor  37845  prjspval2  42636  trclfvcom  43747  scottrankd  44272  meaiininclem  46515  carageniuncllem2  46551  hoidmv1le  46623  hoidmvle  46629  ovnhoilem2  46631  ovnhoi  46632  ovnlecvr2  46639  ovncvr2  46640  hspmbl  46658  ovolval4lem1  46678  ovnovollem1  46685  ovnovollem2  46686  iunhoiioo  46705  vonioolem2  46710  smflimlem4  46803  smflimlem6  46805