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

Theorem reubidva 2883
 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:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem reubidva
StepHypRef Expression
1 nfv 1629 . 2
2 reubidva.1 . 2
31, 2reubida 2882 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wcel 1725  wreu 2699 This theorem is referenced by:  reubidv  2884  reuxfr2d  4738  reuxfrd  4740  exfo  5879  riotabidva  6558  f1ofveu  6576  zmax  10563  zbtwnre  10564  rebtwnz  10565  icoshftf1o  11012  divalgb  12916  1arith2  13288  ply1divalg2  20053  addinv  21932  pjhtheu2  22910  reuxfr3d  23968  reuxfr4d  23969  xrmulc1cn  24308  frg2woteu  28381  hdmap14lem14  32619 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761 This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-eu 2284  df-reu 2704
 Copyright terms: Public domain W3C validator