Theorem ral0 4449

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1541  ∀wral 3049  ∅c0 4283

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 2123  ax-ext 2706

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 2713  df-cleq 2726  df-ral 3050  df-dif 3902  df-nul 4284

This theorem is referenced by:  int0  4915  0iin  5017  po0  5547  so0  5568  mpt0  6632  naddrid  8609  ixp0x  8862  ac6sfi  9182  sup0riota  9367  infpssrlem4  10214  axdc3lem4  10361  0tsk  10664  uzsupss  12851  xrsupsslem  13220  xrinfmsslem  13221  xrsup0  13236  fsuppmapnn0fiubex  13913  swrd0  14580  swrdspsleq  14587  repswsymballbi  14701  cshw1  14743  rexfiuz  15269  lcmf0  16559  2prm  16617  0ssc  17759  0subcat  17760  drsdirfi  18226  0pos  18242  mrelatglb0  18482  s1chn  18541  chnub  18543  sgrp0b  18651  ga0  19225  psgnunilem3  19423  lbsexg  21117  ocv0  21630  mdetunilem9  22562  imasdsf1olem  24315  prdsxmslem2  24471  lebnumlem3  24916  cniccbdd  25416  ovolicc2lem4  25475  c1lip1  25956  ulm0  26354  rightpos  27809  precsexlem9  28183  n0sfincut  28315  zscut  28365  twocut  28381  addhalfcut  28416  0reno  28441  istrkg2ld  28481  nbgr1vtx  29380  cplgr0  29447  cplgr1v  29452  wwlksn0s  29883  clwwlkn  30050  clwwlkn1  30065  0ewlk  30138  1ewlk  30139  0wlk  30140  0conngr  30216  frgr0v  30286  frgr0  30289  frgr1v  30295  1vwmgr  30300  chocnul  31352  locfinref  33947  esumnul  34154  derang0  35312  unt0  35854  fdc  37885  lub0N  39388  glb0N  39392  0psubN  39948  sticksstones11  42349  cantnfresb  43508  safesnsupfilb  43601  nla0002  43607  nla0003  43608  iso0  44490  fnchoice  45216  eliuniincex  45295  eliincex  45296  limcdm0  45806  2ffzoeq  47515  iccpartiltu  47610  iccpartigtl  47611  0mgm  48354  linds0  48653  0funcALT  49275  0thincg  49645  termolmd  49857