MPE Home 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
21adantr 465 . 2
32reubidva 3041 1
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
  Copyright terms: Public domain W3C validator