Theorem ral0 4027

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.)

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

Step	Hyp	Ref	Expression
1		noel 3877	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 114	. 2 ⊢ (𝑥 ∈ ∅ → 𝜑)
3	2	rgen 2905	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

Syntax hints:   ∈ wcel 1976  ∀wral 2895  ∅c0 3873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174  df-dif 3542  df-nul 3874

This theorem is referenced by:  int0  4419  0iin  4508  po0  4964  so0  4982  mpt0  5920  ixp0x  7799  ac6sfi  8066  sup0riota  8231  infpssrlem4  8988  axdc3lem4  9135  0tsk  9433  uzsupss  11612  xrsupsslem  11965  xrinfmsslem  11966  xrsup0  11981  fsuppmapnn0fiubex  12609  swrd0  13232  swrdspsleq  13247  repswsymballbi  13324  cshw1  13365  rexfiuz  13881  lcmf0  15131  2prm  15189  0ssc  16266  0subcat  16267  drsdirfi  16707  0pos  16723  mrelatglb0  16954  mgm0  17024  sgrp0  17060  sgrp0b  17061  ga0  17500  psgnunilem3  17685  lbsexg  18931  ocv0  19782  mdetunilem9  20187  imasdsf1olem  21929  prdsxmslem2  22085  lebnumlem3  22501  cniccbdd  22954  ovolicc2lem4  23012  c1lip1  23481  ulm0  23866  istrkg2ld  25076  cusgra0v  25755  cusgra1v  25756  uvtx0  25785  0wlk  25841  0trl  25842  0conngra  25968  wwlkn0s  25999  0vgrargra  26230  eupa0  26267  frgra0v  26286  frgra1v  26291  1vwmgra  26296  chocnul  27377  locfinref  29042  esumnul  29243  derang0  30211  unt0  30648  nofulllem1  30907  fdc  32507  lub0N  33290  glb0N  33294  0psubN  33849  iso0  37324  fnchoice  38007  eliuniincex  38119  eliincex  38120  limcdm0  38482  iccpartiltu  39758  iccpartigtl  39759  2ffzoeq  40181  nbgr0vtx  40573  nbgr1vtx  40575  uvtxa01vtx0  40618  cplgr0  40642  cplgr0v  40644  cplgr1v  40647  wwlksn0s  41052  0ewlk  41277  1ewlk  41278  01wlk  41279  0conngr  41354  0vconngr  41355  frgr0v  41428  frgr0  41431  frgr1v  41436  1vwmgr  41441  0mgm  41559  linds0  42043