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

Theorem reubii 2886
 Description: Formula-building rule for restricted existential quantifier (inference rule). (Contributed by NM, 22-Oct-1999.)
Hypothesis
Ref Expression
reubii.1
Assertion
Ref Expression
reubii

Proof of Theorem reubii
StepHypRef Expression
1 reubii.1 . . 3
21a1i 11 . 2
32reubiia 2885 1
 Colors of variables: wff set class Syntax hints:   wb 177   wcel 1725  wreu 2699 This theorem is referenced by:  2reu5lem1  3131  reusv2lem5  4720  reusv2  4721  reusv5OLD  4725  reusv7OLD  4727  oaf1o  6798  aceq2  7992  spwex  14653  usgraidx2vlem1  21402  usgraidx2vlem2  21403  cnlnadjlem3  23564  disjrdx  24023  2reu7  27926  2reu8  27927  frgraunss  28312  frgraun  28313  n4cyclfrgra  28335  lshpsmreu  29834 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-tru 1328  df-ex 1551  df-nf 1554  df-eu 2284  df-reu 2704
 Copyright terms: Public domain W3C validator