Theorem ral0 3887

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 3744	. . 3 |- -. x e. (/)
2	1	pm2.21i 131	. 2 |- ( x e. (/) -> ph )
3	2	rgen 2893	1 |- A. x e. (/) ph

Syntax hints:   e. wcel 1758   A.wral 2796   (/)c0 3740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ral 2801  df-v 3074  df-dif 3434  df-nul 3741

This theorem is referenced by:  0iin  4331  reusv6OLD  4606  reusv7OLD  4607  po0  4759  so0  4777  mpt0  5641  ixp0x  7396  ac6sfi  7662  infpssrlem4  8581  axdc3lem4  8728  0tsk  9028  uzsupss  11053  xrsupsslem  11375  xrinfmsslem  11376  xrsup0  11392  swrdspsleq  12455  repswsymballbi  12531  cshw1  12569  rexfiuz  12948  2prm  13892  drsdirfi  15222  0pos  15238  mrelatglb0  15469  ga0  15930  psgnunilem3  16116  lbsexg  17363  ocv0  18222  mdetunilem9  18553  imasdsf1olem  20075  prdsxmslem2  20231  lebnumlem3  20662  cniccbdd  21072  ovolicc2lem4  21130  c1lip1  21597  ulm0  21984  istrkg2ld  23050  cusgra0v  23515  cusgra1v  23516  uvtx0  23546  0wlk  23591  0trl  23592  0conngra  23707  eupa0  23742  chocnul  24878  esumnul  26642  derang0  27196  unt0  27501  nofulllem1  27982  fdc  28784  iso0  29736  fnchoice  29894  2ffzoeq  30357  wwlkn0s  30482  0vgrargra  30693  frgra0v  30728  frgra1v  30733  1vwmgra  30738  fsuppmapnn0fiubex  30943  linds0  31113  lub0N  33153  glb0N  33157  0psubN  33712