Theorem ral0 4513

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1539  ∀wral 3059  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-ral 3060  df-dif 3952  df-nul 4324

This theorem is referenced by:  int0  4967  0iin  5068  po0  5606  so0  5625  mpt0  6693  naddrid  8686  ixp0x  8924  ac6sfi  9291  sup0riota  9464  infpssrlem4  10305  axdc3lem4  10452  0tsk  10754  uzsupss  12930  xrsupsslem  13292  xrinfmsslem  13293  xrsup0  13308  fsuppmapnn0fiubex  13963  swrd0  14614  swrdspsleq  14621  repswsymballbi  14736  cshw1  14778  rexfiuz  15300  lcmf0  16577  2prm  16635  0ssc  17793  0subcat  17794  drsdirfi  18264  0pos  18280  0posOLD  18281  mrelatglb0  18520  sgrp0b  18655  ga0  19205  psgnunilem3  19407  lbsexg  20924  ocv0  21451  mdetunilem9  22344  imasdsf1olem  24101  prdsxmslem2  24260  lebnumlem3  24711  cniccbdd  25212  ovolicc2lem4  25271  c1lip1  25748  ulm0  26137  precsexlem9  27898  istrkg2ld  27976  nbgr0vtx  28878  nbgr1vtx  28880  cplgr0  28947  cplgr1v  28952  wwlksn0s  29380  clwwlkn  29544  clwwlkn1  29559  0ewlk  29632  1ewlk  29633  0wlk  29634  0conngr  29710  frgr0v  29780  frgr0  29783  frgr1v  29789  1vwmgr  29794  chocnul  30846  locfinref  33117  esumnul  33342  derang0  34456  unt0  34982  fdc  36918  lub0N  38364  glb0N  38368  0psubN  38925  sticksstones11  41280  cantnfresb  42378  safesnsupfilb  42473  nla0002  42479  nla0003  42480  iso0  43370  fnchoice  44017  eliuniincex  44101  eliincex  44102  limcdm0  44634  2ffzoeq  46336  iccpartiltu  46390  iccpartigtl  46391  0mgm  46844  linds0  47235  0thincg  47759