Theorem ral0 4462

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1541  ∀wral 3047  ∅c0 4282

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 2121  ax-ext 2703

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 2710  df-cleq 2723  df-ral 3048  df-dif 3900  df-nul 4283

This theorem is referenced by:  int0  4912  0iin  5014  po0  5544  so0  5565  mpt0  6629  naddrid  8604  ixp0x  8856  ac6sfi  9174  sup0riota  9356  infpssrlem4  10203  axdc3lem4  10350  0tsk  10652  uzsupss  12844  xrsupsslem  13212  xrinfmsslem  13213  xrsup0  13228  fsuppmapnn0fiubex  13905  swrd0  14572  swrdspsleq  14579  repswsymballbi  14693  cshw1  14735  rexfiuz  15261  lcmf0  16551  2prm  16609  0ssc  17750  0subcat  17751  drsdirfi  18217  0pos  18233  mrelatglb0  18473  s1chn  18532  chnub  18534  sgrp0b  18642  ga0  19216  psgnunilem3  19414  lbsexg  21107  ocv0  21620  mdetunilem9  22541  imasdsf1olem  24294  prdsxmslem2  24450  lebnumlem3  24895  cniccbdd  25395  ovolicc2lem4  25454  c1lip1  25935  ulm0  26333  rightpos  27788  precsexlem9  28159  n0sfincut  28288  zscut  28337  twocut  28352  addhalfcut  28385  istrkg2ld  28444  nbgr1vtx  29343  cplgr0  29410  cplgr1v  29415  wwlksn0s  29846  clwwlkn  30013  clwwlkn1  30028  0ewlk  30101  1ewlk  30102  0wlk  30103  0conngr  30179  frgr0v  30249  frgr0  30252  frgr1v  30258  1vwmgr  30263  chocnul  31315  locfinref  33861  esumnul  34068  derang0  35220  unt0  35762  fdc  37791  lub0N  39294  glb0N  39298  0psubN  39854  sticksstones11  42255  cantnfresb  43422  safesnsupfilb  43516  nla0002  43522  nla0003  43523  iso0  44405  fnchoice  45131  eliuniincex  45211  eliincex  45212  limcdm0  45723  2ffzoeq  47432  iccpartiltu  47527  iccpartigtl  47528  0mgm  48271  linds0  48571  0funcALT  49194  0thincg  49564  termolmd  49776