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

Theorem ral0 3558
Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)
Assertion
Ref Expression
ral0  |-  A. x  e.  (/)  ph

Proof of Theorem ral0
StepHypRef Expression
1 noel 3459 . . 3  |-  -.  x  e.  (/)
21pm2.21i 123 . 2  |-  ( x  e.  (/)  ->  ph )
32rgen 2608 1  |-  A. x  e.  (/)  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   A.wral 2543   (/)c0 3455
This theorem is referenced by:  0iin  3960  po0  4329  so0  4347  reusv6OLD  4545  reusv7OLD  4546  mpt0  5371  ixp0x  6844  ac6sfi  7101  infpssrlem4  7932  axdc3lem4  8079  0tsk  8377  uzsupss  10310  xrsupsslem  10625  xrinfmsslem  10626  xrsup0  10642  rexfiuz  11831  2prm  12774  drsdirfi  14072  0pos  14088  mrelatglb0  14288  ga0  14752  lbsexg  15917  ocv0  16577  imasdsf1olem  17937  prdsxmslem2  18075  lebnumlem3  18461  cniccbdd  18821  ovolicc2lem4  18879  c1lip1  19344  ulm0  19770  chocnul  21907  esumnul  23427  derang0  23700  eupa0  23898  unt0  24057  nofulllem1  24356  vutr  24950  fdc  26455  psgnunilem3  27419  iso0  27536  fnchoice  27700  cusgra0v  28156  cusgra1v  28157  uvtx0  28163  frgra0v  28174  frgra1v  28176  1vwmgra  28181  lub0N  29379  glb0N  29383  0psubN  29938
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-dif 3155  df-nul 3456
  Copyright terms: Public domain W3C validator