Theorem ral0 4458

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1568  ∀wral 3077  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-ral 3078  df-dif 3907  df-nul 4286

This theorem is referenced by:  int0  4926  0iin  5027  po0  5586  so0  5607  mpt0  6677  naddrid  8669  ixp0x  8923  ac6sfi  9243  sup0riota  9425  infpssrlem4  10289  axdc3lem4  10436  0tsk  10739  uzsupss  12963  xrsupsslem  13332  xrinfmsslem  13333  xrsup0  13348  fsuppmapnn0fiubex  14027  swrd0  14695  swrdspsleq  14702  repswsymballbi  14816  cshw1  14858  rexfiuz  15398  lcmf0  16691  2prm  16749  0ssc  17893  0subcat  17894  drsdirfi  18360  0pos  18376  mrelatglb0  18616  s1chn  18675  chnub  18677  sgrp0b  18785  ga0  19367  psgnunilem3  19565  lbsexg  21267  ocv0  21806  mdetunilem9  22756  imasdsf1olem  24509  prdsxmslem2  24665  lebnumlem3  25101  cniccbdd  25599  ovolicc2lem4  25658  c1lip1  26135  ulm0  26530  rightge0  27990  precsexlem9  28384  onsbnd  28450  n0fincut  28524  zcuts  28576  twocut  28592  addhalfcut  28628  0reno  28665  istrkg2ld  28705  nbgr1vtx  29674  cplgr0  29741  cplgr1v  29746  wwlksn0s  30176  clwwlkn  30343  clwwlkn1  30358  0ewlk  30431  1ewlk  30432  0wlk  30433  0conngr  30509  frgr0v  30579  frgr0  30582  frgr1v  30588  1vwmgr  30593  chocnul  31646  locfinref  34197  esumnul  34404  derang0  35615  unt0  36157  nmulr0  36641  fdc  38340  lub0N  39909  glb0N  39913  0psubN  40469  sticksstones11  42869  cantnfresb  43999  safesnsupfilb  44092  nla0002  44098  nla0003  44099  iso0  44965  fnchoice  45697  eliuniincex  45775  eliincex  45776  limcdm0  46282  2ffzoeq  48010  iccpartiltu  48116  iccpartigtl  48117  0mgm  48876  linds0  49190  0funcALT  49811  0thincg  50181  termolmd  50393