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

Theorem reubii 3044
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 3043 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  e.wcel 1818  E!wreu 2809
This theorem is referenced by:  2reu5lem1  3305  reusv2lem5  4657  reusv2  4658  reusv5OLD  4662  reusv7OLD  4664  oaf1o  7231  aceq2  8521  lubfval  15608  lubeldm  15611  glbfval  15621  glbeldm  15624  oduglb  15769  odulub  15771  usgraidx2vlem1  24391  usgraidx2vlem2  24392  frgraunss  24995  frgraun  24996  n4cyclfrgra  25018  cnlnadjlem3  26988  disjrdx  27450  2reu7  32196  2reu8  32197  usgedgvadf1lem1  32413  usgedgvadf1lem2  32414  usgedgvadf1ALTlem1  32416  usgedgvadf1ALTlem2  32417  lshpsmreu  34834
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-tru 1398  df-ex 1613  df-nf 1617  df-eu 2286  df-reu 2814
  Copyright terms: Public domain W3C validator