Theorem ral0 4453

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

This proof depends on syntax axioms:   = wceq 1569  ∀wral 3076  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-ral 3077  df-dif 4046  df-nul 4278

This theorem is used by:  int0  4921  0iin  5021  po0  5576  so0  5597  mpt0  6686  naddrid  8700  ixp0x  8961  ac6sfi  9282  sup0riota  9465  infpssrlem4  10391  axdc3lem4  10538  0tsk  10847  uzsupss  13074  xrsupsslem  13444  xrinfmsslem  13445  xrsup0  13460  fsuppmapnn0fiubex  14142  swrd0  14816  swrdspsleq  14823  repswsymballbi  14939  cshw1  14981  rexfiuz  15524  lcmf0  16818  2prm  16876  0ssc  18021  0subcat  18022  drsdirfi  18488  0pos  18504  mrelatglb0  18744  s1chn  18803  chnub  18805  sgrp0b  18926  ga0  19521  psgnunilem3  19719  lbsexg  21451  ocv0  21992  mdetunilem9  22944  imasdsf1olem  24701  prdsxmslem2  24857  lebnumlem3  25293  cniccbdd  25791  ovolicc2lem4  25850  c1lip1  26326  ulm0  26727  rightge0  28216  precsexlem9  28610  onsbnd  28676  n0fincut  28750  zcuts  28802  twocut  28818  addhalfcut  28854  0reno  28891  istrkg2ld  28931  nbgr1vtx  29948  cplgr0  30015  cplgr1v  30020  wwlksn0s  30459  clwwlkn  30626  clwwlkn1  30641  0ewlk  30714  1ewlk  30715  0wlk  30716  0conngr  30802  frgr0v  30872  frgr0  30875  frgr1v  30881  1vwmgr  30886  chocnul  31939  locfinref  34523  esumnul  34730  derang0  36024  unt0  36572  nmulr0  37040  mh-inf3f1  37425  fdc  38788  lub0N  40355  glb0N  40359  0psubN  40915  sticksstones11  43315  cantnfresb  44435  safesnsupfilb  44528  nla0002  44534  nla0003  44535  iso0  45400  fnchoice  46154  eliuniincex  46232  eliincex  46233  limcdm0  46738  2ffzoeq  48506  iccpartiltu  48612  iccpartigtl  48613  0mgm  49371  linds0  49685  0funcALT  50311  0thincg  50701  termolmd  50961