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

Theorem reubidv 3042
 Description: Formula-building rule for restricted existential quantifier (deduction rule). (Contributed by NM, 17-Oct-1996.)
Hypothesis
Ref Expression
reubidv.1
Assertion
Ref Expression
reubidv
Distinct variable group:   ,

Proof of Theorem reubidv
StepHypRef Expression
1 reubidv.1 . . 3
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  E!wreu 2809 This theorem is referenced by:  reueqd  3064  sbcreu  3414  sbcreugOLD  3415  reusv6OLD  4663  reusv7OLD  4664  oawordeu  7223  xpf1o  7699  dfac2  8532  creur  10555  creui  10556  divalg  14061  divalg2  14063  lubfval  15608  lubeldm  15611  lubval  15614  glbfval  15621  glbeldm  15624  glbval  15627  joineu  15640  meeteu  15654  dfod2  16586  ustuqtop  20749  isfrgra  24990  frgraunss  24995  frgra1v  24998  frgra2v  24999  frgra3v  25002  3vfriswmgra  25005  n4cyclfrgra  25018  riesz4  26983  cnlnadjeu  26997  hdmap1eulem  37551  hdmap1eulemOLDN  37552  hdmap14lem6  37603 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