Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  reubidva Unicode version

Theorem reubidva 3041
 Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 13-Nov-2004.)
Hypothesis
Ref Expression
reubidva.1
Assertion
Ref Expression
reubidva
Distinct variable group:   ,

Proof of Theorem reubidva
StepHypRef Expression
1 nfv 1707 . 2
2 reubidva.1 . 2
31, 2reubida 3040 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  e.wcel 1818  E!wreu 2809 This theorem is referenced by:  reubidv  3042  reuxfr2d  4675  reuxfrd  4677  exfo  6049  f1ofveu  6291  zmax  11208  zbtwnre  11209  rebtwnz  11210  icoshftf1o  11672  divalgb  14062  1arith2  14446  ply1divalg2  22539  frg2woteu  25055  numclwwlk2lem1  25102  numclwlk2lem2f1o  25105  addinv  25354  pjhtheu2  26334  reuxfr3d  27388  reuxfr4d  27389  xrsclat  27668  xrmulc1cn  27912  hdmap14lem14  37611 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-12 1854 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617  df-eu 2286  df-reu 2814
 Copyright terms: Public domain W3C validator