Theorem ral0 4460

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) Avoid df-clel 2806, ax-8 2113. (Revised by GG, 2-Sep-2024.)

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

Step	Hyp	Ref	Expression
1		eqid 2731	. 2 ⊢ ∅ = ∅
2		rzal 4456	. 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

Syntax hints:   = wceq 1541  ∀wral 3047  ∅c0 4280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-ral 3048  df-dif 3900  df-nul 4281

This theorem is referenced by:  int0  4910  0iin  5010  po0  5539  so0  5560  mpt0  6623  naddrid  8598  ixp0x  8850  ac6sfi  9168  sup0riota  9350  infpssrlem4  10197  axdc3lem4  10344  0tsk  10646  uzsupss  12838  xrsupsslem  13206  xrinfmsslem  13207  xrsup0  13222  fsuppmapnn0fiubex  13899  swrd0  14566  swrdspsleq  14573  repswsymballbi  14687  cshw1  14729  rexfiuz  15255  lcmf0  16545  2prm  16603  0ssc  17744  0subcat  17745  drsdirfi  18211  0pos  18227  mrelatglb0  18467  s1chn  18526  chnub  18528  sgrp0b  18636  ga0  19210  psgnunilem3  19408  lbsexg  21101  ocv0  21614  mdetunilem9  22535  imasdsf1olem  24288  prdsxmslem2  24444  lebnumlem3  24889  cniccbdd  25389  ovolicc2lem4  25448  c1lip1  25929  ulm0  26327  rightpos  27782  precsexlem9  28153  n0sfincut  28282  zscut  28331  twocut  28346  addhalfcut  28379  istrkg2ld  28438  nbgr1vtx  29336  cplgr0  29403  cplgr1v  29408  wwlksn0s  29839  clwwlkn  30006  clwwlkn1  30021  0ewlk  30094  1ewlk  30095  0wlk  30096  0conngr  30172  frgr0v  30242  frgr0  30245  frgr1v  30251  1vwmgr  30256  chocnul  31308  locfinref  33854  esumnul  34061  derang0  35213  unt0  35755  fdc  37793  lub0N  39236  glb0N  39240  0psubN  39796  sticksstones11  42197  cantnfresb  43365  safesnsupfilb  43459  nla0002  43465  nla0003  43466  iso0  44348  fnchoice  45074  eliuniincex  45154  eliincex  45155  limcdm0  45666  2ffzoeq  47366  iccpartiltu  47461  iccpartigtl  47462  0mgm  48205  linds0  48505  0funcALT  49128  0thincg  49498  termolmd  49710