Theorem ral0 4476

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1540  ∀wral 3044  ∅c0 4296

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-ral 3045  df-dif 3917  df-nul 4297

This theorem is referenced by:  int0  4926  0iin  5028  po0  5563  so0  5584  mpt0  6660  naddrid  8647  ixp0x  8899  ac6sfi  9231  sup0riota  9417  infpssrlem4  10259  axdc3lem4  10406  0tsk  10708  uzsupss  12899  xrsupsslem  13267  xrinfmsslem  13268  xrsup0  13283  fsuppmapnn0fiubex  13957  swrd0  14623  swrdspsleq  14630  repswsymballbi  14745  cshw1  14787  rexfiuz  15314  lcmf0  16604  2prm  16662  0ssc  17799  0subcat  17800  drsdirfi  18266  0pos  18282  mrelatglb0  18520  sgrp0b  18655  ga0  19230  psgnunilem3  19426  lbsexg  21074  ocv0  21586  mdetunilem9  22507  imasdsf1olem  24261  prdsxmslem2  24417  lebnumlem3  24862  cniccbdd  25362  ovolicc2lem4  25421  c1lip1  25902  ulm0  26300  precsexlem9  28117  n0sfincut  28246  zscut  28295  twocut  28309  addhalfcut  28334  istrkg2ld  28387  nbgr1vtx  29285  cplgr0  29352  cplgr1v  29357  wwlksn0s  29791  clwwlkn  29955  clwwlkn1  29970  0ewlk  30043  1ewlk  30044  0wlk  30045  0conngr  30121  frgr0v  30191  frgr0  30194  frgr1v  30200  1vwmgr  30205  chocnul  31257  s1chn  32936  chnub  32938  locfinref  33831  esumnul  34038  derang0  35156  unt0  35698  fdc  37739  lub0N  39182  glb0N  39186  0psubN  39743  sticksstones11  42144  cantnfresb  43313  safesnsupfilb  43407  nla0002  43413  nla0003  43414  iso0  44296  fnchoice  45023  eliuniincex  45103  eliincex  45104  limcdm0  45616  2ffzoeq  47328  iccpartiltu  47423  iccpartigtl  47424  0mgm  48154  linds0  48454  0funcALT  49077  0thincg  49447  termolmd  49659