Theorem ral0 4464

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1567  ∀wral 3085  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-ral 3086  df-dif 3916  df-nul 4295

This theorem is referenced by:  int0  4931  0iin  5032  po0  5587  so0  5608  mpt0  6678  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  21265  ocv0  21795  mdetunilem9  22745  imasdsf1olem  24498  prdsxmslem2  24654  lebnumlem3  25090  cniccbdd  25588  ovolicc2lem4  25647  c1lip1  26124  ulm0  26519  rightge0  27979  precsexlem9  28373  onsbnd  28439  n0fincut  28513  zcuts  28565  twocut  28581  addhalfcut  28617  0reno  28654  istrkg2ld  28694  nbgr1vtx  29648  cplgr0  29715  cplgr1v  29720  wwlksn0s  30150  clwwlkn  30317  clwwlkn1  30332  0ewlk  30405  1ewlk  30406  0wlk  30407  0conngr  30483  frgr0v  30553  frgr0  30556  frgr1v  30562  1vwmgr  30567  chocnul  31620  locfinref  34175  esumnul  34382  derang0  35559  unt0  36101  nmulr0  36585  fdc  38283  lub0N  39852  glb0N  39856  0psubN  40412  sticksstones11  42812  cantnfresb  43942  safesnsupfilb  44035  nla0002  44041  nla0003  44042  iso0  44908  fnchoice  45640  eliuniincex  45718  eliincex  45719  limcdm0  46225  2ffzoeq  47953  iccpartiltu  48059  iccpartigtl  48060  0mgm  48819  linds0  49129  0funcALT  49750  0thincg  50120  termolmd  50332