Theorem ral0 3932

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

Step	Hyp	Ref	Expression
1		noel 3789	. . 3 |- -. x e. (/)
2	1	pm2.21i 131	. 2 |- ( x e. (/) -> ph )
3	2	rgen 2824	1 |- A. x e. (/) ph

Syntax hints:   e. wcel 1767   A.wral 2814   (/)c0 3785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115  df-dif 3479  df-nul 3786

This theorem is referenced by:  0iin  4383  reusv6OLD  4658  reusv7OLD  4659  po0  4815  so0  4833  mpt0  5708  ixp0x  7497  ac6sfi  7764  infpssrlem4  8686  axdc3lem4  8833  0tsk  9133  uzsupss  11174  xrsupsslem  11498  xrinfmsslem  11499  xrsup0  11515  fsuppmapnn0fiubex  12066  swrdspsleq  12636  repswsymballbi  12715  cshw1  12753  rexfiuz  13143  2prm  14092  drsdirfi  15425  0pos  15441  mrelatglb0  15672  ga0  16141  psgnunilem3  16327  lbsexg  17610  ocv0  18503  mdetunilem9  18917  imasdsf1olem  20639  prdsxmslem2  20795  lebnumlem3  21226  cniccbdd  21636  ovolicc2lem4  21694  c1lip1  22161  ulm0  22548  istrkg2ld  23614  cusgra0v  24164  cusgra1v  24165  uvtx0  24195  0wlk  24251  0trl  24252  0conngra  24378  wwlkn0s  24409  0vgrargra  24641  eupa0  24678  frgra0v  24697  frgra1v  24702  1vwmgra  24707  chocnul  25950  esumnul  27727  derang0  28281  unt0  28586  nofulllem1  29067  fdc  29869  iso0  30818  fnchoice  31010  limcdm0  31188  2ffzoeq  31836  linds0  32165  lub0N  34004  glb0N  34008  0psubN  34563