Theorem ral0 4457

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

This proof depends on syntax axioms:   = wceq 1570  ∀wral 3080  ∅c0 4281

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-ral 3081  df-dif 4050  df-nul 4282

This theorem is used by:  int0  4927  0iin  5027  po0  5583  so0  5604  mpt0  6711  naddrid  8731  ixp0x  8992  ac6sfi  9313  sup0riota  9495  infpssrlem4  10423  axdc3lem4  10570  0tsk  10879  uzsupss  13107  xrsupsslem  13477  xrinfmsslem  13478  xrsup0  13493  fsuppmapnn0fiubex  14175  swrd0  14850  swrdspsleq  14857  repswsymballbi  14973  cshw1  15015  rexfiuz  15559  lcmf0  16853  2prm  16911  0ssc  18062  0subcat  18063  drsdirfi  18529  0pos  18545  mrelatglb0  18785  s1chn  18844  chnub  18846  sgrp0b  18967  ga0  19563  psgnunilem3  19761  lbsexg  21493  ocv0  22038  mdetunilem9  22990  imasdsf1olem  24747  prdsxmslem2  24903  lebnumlem3  25339  cniccbdd  25837  ovolicc2lem4  25896  c1lip1  26372  ulm0  26775  rightge0  28264  precsexlem9  28658  onsbnd  28724  n0fincut  28798  zcuts  28850  twocut  28866  addhalfcut  28902  0reno  28939  istrkg2ld  28979  nbgr1vtx  29996  cplgr0  30063  cplgr1v  30068  wwlksn0s  30507  clwwlkn  30674  clwwlkn1  30689  0ewlk  30762  1ewlk  30763  0wlk  30764  0conngr  30850  frgr0v  30920  frgr0  30923  frgr1v  30929  1vwmgr  30934  chocnul  31987  locfinref  34584  esumnul  34791  derang0  36142  unt0  36691  nmulr0  37159  mh-inf3f1  37544  fdc  38945  lub0N  40512  glb0N  40516  0psubN  41072  sticksstones11  43472  cantnfresb  44587  safesnsupfilb  44680  nla0002  44686  nla0003  44687  iso0  45552  fnchoice  46320  eliuniincex  46397  eliincex  46398  limcdm0  46903  2ffzoeq  48671  iccpartiltu  48777  iccpartigtl  48778  0mgm  49536  linds0  49908  0funcALT  50534  0thincg  50924  termolmd  51184