MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iuneq2dv Structured version   Visualization version   GIF version

Theorem iuneq2dv 4934
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
StepHypRef Expression
1 iuneq2dv.1 . . 3 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
21ralrimiva 3180 . 2 (𝜑 → ∀𝑥𝐴 𝐵 = 𝐶)
3 iuneq2 4929 . 2 (∀𝑥𝐴 𝐵 = 𝐶 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
42, 3syl 17 1 (𝜑 𝑥𝐴 𝐵 = 𝑥𝐴 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398   = wceq 1531  wcel 2108  wral 3136   ciun 4910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-v 3495  df-in 3941  df-ss 3950  df-iun 4912
This theorem is referenced by:  iuneq12d  4938  iuneq2d  4939  fparlem3  7801  fparlem4  7802  oalim  8149  omlim  8150  oelim  8151  oelim2  8213  r1val3  9259  imasdsval  16780  acsfn  16922  tgidm  21580  cmpsub  22000  alexsublem  22644  bcth3  23926  ovoliunlem1  24095  voliunlem1  24143  uniiccdif  24171  uniioombllem2  24176  uniioombllem3a  24177  uniioombllem4  24179  itg2monolem1  24343  taylpfval  24945  ofpreima2  30403  fnpreimac  30408  esum2dlem  31344  eulerpartlemgu  31628  cvmscld  32513  satom  32596  msubvrs  32800  mblfinlem2  34922  ftc1anclem6  34964  heibor  35091  prjspval2  39254  trclfvcom  40059  scottrankd  40575  meaiininclem  42759  carageniuncllem2  42795  hoidmv1le  42867  hoidmvle  42873  ovnhoilem2  42875  ovnhoi  42876  ovnlecvr2  42883  ovncvr2  42884  hspmbl  42902  ovolval4lem1  42922  ovnovollem1  42929  ovnovollem2  42930  iunhoiioo  42949  vonioolem2  42954  smflimlem4  43041  smflimlem6  43043
  Copyright terms: Public domain W3C validator