Theorem ral0 4454

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

This proof depends on syntax axioms:   = wceq 1570  ∀wral 3076  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-ral 3077  df-dif 3902  df-nul 4280

This theorem is used by:  int0  4922  0iin  5022  po0  5580  so0  5601  mpt0  6674  naddrid  8672  ixp0x  8933  ac6sfi  9254  sup0riota  9436  infpssrlem4  10308  axdc3lem4  10455  0tsk  10764  uzsupss  12989  xrsupsslem  13359  xrinfmsslem  13360  xrsup0  13375  fsuppmapnn0fiubex  14056  swrd0  14728  swrdspsleq  14735  repswsymballbi  14851  cshw1  14893  rexfiuz  15435  lcmf0  16724  2prm  16782  0ssc  17926  0subcat  17927  drsdirfi  18393  0pos  18409  mrelatglb0  18649  s1chn  18708  chnub  18710  sgrp0b  18830  ga0  19425  psgnunilem3  19623  lbsexg  21351  ocv0  21890  mdetunilem9  22842  imasdsf1olem  24599  prdsxmslem2  24755  lebnumlem3  25191  cniccbdd  25689  ovolicc2lem4  25748  c1lip1  26224  ulm0  26627  rightge0  28086  precsexlem9  28480  onsbnd  28546  n0fincut  28620  zcuts  28672  twocut  28688  addhalfcut  28724  0reno  28761  istrkg2ld  28801  nbgr1vtx  29818  cplgr0  29885  cplgr1v  29890  wwlksn0s  30329  clwwlkn  30496  clwwlkn1  30511  0ewlk  30584  1ewlk  30585  0wlk  30586  0conngr  30672  frgr0v  30742  frgr0  30745  frgr1v  30751  1vwmgr  30756  chocnul  31809  locfinref  34351  esumnul  34558  derang0  35748  unt0  36290  nmulr0  36775  fdc  38495  lub0N  40062  glb0N  40066  0psubN  40622  sticksstones11  43022  cantnfresb  44165  safesnsupfilb  44258  nla0002  44264  nla0003  44265  iso0  45131  fnchoice  45863  eliuniincex  45941  eliincex  45942  limcdm0  46448  2ffzoeq  48216  iccpartiltu  48322  iccpartigtl  48323  0mgm  49081  linds0  49395  0funcALT  50014  0thincg  50384  termolmd  50596