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

Theorem ral0 3668
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 3568 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  ph )
32rgen 2707 1  |-  A. x  e.  (/)  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   A.wral 2642   (/)c0 3564
This theorem is referenced by:  0iin  4083  po0  4452  so0  4470  reusv6OLD  4667  reusv7OLD  4668  mpt0  5505  ixp0x  7019  ac6sfi  7280  infpssrlem4  8112  axdc3lem4  8259  0tsk  8556  uzsupss  10493  xrsupsslem  10810  xrinfmsslem  10811  xrsup0  10827  rexfiuz  12071  2prm  13015  drsdirfi  14315  0pos  14331  mrelatglb0  14531  ga0  14995  lbsexg  16156  ocv0  16820  imasdsf1olem  18304  prdsxmslem2  18442  lebnumlem3  18852  cniccbdd  19218  ovolicc2lem4  19276  c1lip1  19741  ulm0  20167  cusgra0v  21328  cusgra1v  21329  uvtx0  21359  0wlk  21402  0trl  21403  0conngra  21502  eupa0  21537  chocnul  22671  esumnul  24232  derang0  24627  unt0  24932  nofulllem1  25373  fdc  26133  psgnunilem3  27081  iso0  27198  fnchoice  27361  frgra0v  27739  frgra1v  27744  1vwmgra  27749  lub0N  29355  glb0N  29359  0psubN  29914
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647  df-v 2894  df-dif 3259  df-nul 3565
  Copyright terms: Public domain W3C validator