Theorem ral0 4464

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 4460	. 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

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

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 3906  df-nul 4285

This theorem is referenced by:  int0  4912  0iin  5013  po0  5544  so0  5565  mpt0  6624  naddrid  8601  ixp0x  8853  ac6sfi  9173  sup0riota  9356  infpssrlem4  10200  axdc3lem4  10347  0tsk  10649  uzsupss  12841  xrsupsslem  13209  xrinfmsslem  13210  xrsup0  13225  fsuppmapnn0fiubex  13899  swrd0  14565  swrdspsleq  14572  repswsymballbi  14686  cshw1  14728  rexfiuz  15255  lcmf0  16545  2prm  16603  0ssc  17744  0subcat  17745  drsdirfi  18211  0pos  18227  mrelatglb0  18467  sgrp0b  18602  ga0  19177  psgnunilem3  19375  lbsexg  21071  ocv0  21584  mdetunilem9  22505  imasdsf1olem  24259  prdsxmslem2  24415  lebnumlem3  24860  cniccbdd  25360  ovolicc2lem4  25419  c1lip1  25900  ulm0  26298  precsexlem9  28122  n0sfincut  28251  zscut  28300  twocut  28315  addhalfcut  28347  istrkg2ld  28405  nbgr1vtx  29303  cplgr0  29370  cplgr1v  29375  wwlksn0s  29806  clwwlkn  29970  clwwlkn1  29985  0ewlk  30058  1ewlk  30059  0wlk  30060  0conngr  30136  frgr0v  30206  frgr0  30209  frgr1v  30215  1vwmgr  30220  chocnul  31272  s1chn  32952  chnub  32954  locfinref  33808  esumnul  34015  derang0  35142  unt0  35684  fdc  37725  lub0N  39168  glb0N  39172  0psubN  39728  sticksstones11  42129  cantnfresb  43297  safesnsupfilb  43391  nla0002  43397  nla0003  43398  iso0  44280  fnchoice  45007  eliuniincex  45087  eliincex  45088  limcdm0  45599  2ffzoeq  47311  iccpartiltu  47406  iccpartigtl  47407  0mgm  48150  linds0  48450  0funcALT  49073  0thincg  49443  termolmd  49655