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

Theorem ral0 3724
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 3624 . . 3  |-  -.  x  e.  (/)
21pm2.21i 125 . 2  |-  ( x  e.  (/)  ->  ph )
32rgen 2763 1  |-  A. x  e.  (/)  ph
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   A.wral 2697   (/)c0 3620
This theorem is referenced by:  0iin  4141  po0  4510  so0  4528  reusv6OLD  4726  reusv7OLD  4727  mpt0  5564  ixp0x  7082  ac6sfi  7343  infpssrlem4  8178  axdc3lem4  8325  0tsk  8622  uzsupss  10560  xrsupsslem  10877  xrinfmsslem  10878  xrsup0  10894  rexfiuz  12143  2prm  13087  drsdirfi  14387  0pos  14403  mrelatglb0  14603  ga0  15067  lbsexg  16228  ocv0  16896  imasdsf1olem  18395  prdsxmslem2  18551  lebnumlem3  18980  cniccbdd  19350  ovolicc2lem4  19408  c1lip1  19873  ulm0  20299  cusgra0v  21461  cusgra1v  21462  uvtx0  21492  0wlk  21537  0trl  21538  0conngra  21653  eupa0  21688  chocnul  22822  esumnul  24435  derang0  24847  unt0  25152  nofulllem1  25649  fdc  26440  psgnunilem3  27387  iso0  27504  fnchoice  27667  cshw1  28238  frgra0v  28320  frgra1v  28325  1vwmgra  28330  lub0N  29924  glb0N  29928  0psubN  30483
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-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950  df-dif 3315  df-nul 3621
  Copyright terms: Public domain W3C validator