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

Theorem ral0 3571
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 3472 . . 3  |-  -.  x  e.  (/)
21pm2.21i 123 . 2  |-  ( x  e.  (/)  ->  ph )
32rgen 2621 1  |-  A. x  e.  (/)  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   A.wral 2556   (/)c0 3468
This theorem is referenced by:  0iin  3976  po0  4345  so0  4363  reusv6OLD  4561  reusv7OLD  4562  mpt0  5387  ixp0x  6860  ac6sfi  7117  infpssrlem4  7948  axdc3lem4  8095  0tsk  8393  uzsupss  10326  xrsupsslem  10641  xrinfmsslem  10642  xrsup0  10658  rexfiuz  11847  2prm  12790  drsdirfi  14088  0pos  14104  mrelatglb0  14304  ga0  14768  lbsexg  15933  ocv0  16593  imasdsf1olem  17953  prdsxmslem2  18091  lebnumlem3  18477  cniccbdd  18837  ovolicc2lem4  18895  c1lip1  19360  ulm0  19786  chocnul  21923  esumnul  23442  derang0  23715  eupa0  23913  unt0  24072  nofulllem1  24427  vutr  25053  fdc  26558  psgnunilem3  27522  iso0  27639  fnchoice  27803  cusgra0v  28295  cusgra1v  28296  uvtx0  28304  0wlk  28343  0trl  28344  frgra0v  28420  frgra1v  28422  1vwmgra  28427  lub0N  30001  glb0N  30005  0psubN  30560
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-dif 3168  df-nul 3469
  Copyright terms: Public domain W3C validator