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

Theorem ral0 3781
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 3638 . . 3  |-  -.  x  e.  (/)
21pm2.21i 131 . 2  |-  ( x  e.  (/)  ->  ph )
32rgen 2779 1  |-  A. x  e.  (/)  ph
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761   A.wral 2713   (/)c0 3634
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ral 2718  df-v 2972  df-dif 3328  df-nul 3635
This theorem is referenced by:  0iin  4225  reusv6OLD  4500  reusv7OLD  4501  po0  4652  so0  4670  mpt0  5535  ixp0x  7287  ac6sfi  7552  infpssrlem4  8471  axdc3lem4  8618  0tsk  8918  uzsupss  10943  xrsupsslem  11265  xrinfmsslem  11266  xrsup0  11282  swrdspsleq  12338  repswsymballbi  12414  cshw1  12452  rexfiuz  12831  2prm  13775  drsdirfi  15104  0pos  15120  mrelatglb0  15351  ga0  15809  psgnunilem3  15995  lbsexg  17223  ocv0  18061  mdetunilem9  18385  imasdsf1olem  19907  prdsxmslem2  20063  lebnumlem3  20494  cniccbdd  20904  ovolicc2lem4  20962  c1lip1  21428  ulm0  21815  cusgra0v  23303  cusgra1v  23304  uvtx0  23334  0wlk  23379  0trl  23380  0conngra  23495  eupa0  23530  chocnul  24666  esumnul  26438  derang0  26987  unt0  27291  nofulllem1  27772  fdc  28566  iso0  29518  fnchoice  29676  2ffzoeq  30139  wwlkn0s  30264  0vgrargra  30475  frgra0v  30510  frgra1v  30515  1vwmgra  30520  linds0  30840  lub0N  32556  glb0N  32560  0psubN  33115
  Copyright terms: Public domain W3C validator