Theorem ral0 4536

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1537  ∀wral 3067  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-ral 3068  df-dif 3979  df-nul 4353

This theorem is referenced by:  int0  4986  0iin  5087  po0  5625  so0  5645  mpt0  6722  naddrid  8739  ixp0x  8984  ac6sfi  9348  sup0riota  9534  infpssrlem4  10375  axdc3lem4  10522  0tsk  10824  uzsupss  13005  xrsupsslem  13369  xrinfmsslem  13370  xrsup0  13385  fsuppmapnn0fiubex  14043  swrd0  14706  swrdspsleq  14713  repswsymballbi  14828  cshw1  14870  rexfiuz  15396  lcmf0  16681  2prm  16739  0ssc  17901  0subcat  17902  drsdirfi  18375  0pos  18391  0posOLD  18392  mrelatglb0  18631  sgrp0b  18766  ga0  19338  psgnunilem3  19538  lbsexg  21189  ocv0  21718  mdetunilem9  22647  imasdsf1olem  24404  prdsxmslem2  24563  lebnumlem3  25014  cniccbdd  25515  ovolicc2lem4  25574  c1lip1  26056  ulm0  26452  precsexlem9  28257  zscut  28411  nohalf  28425  addhalfcut  28437  istrkg2ld  28486  nbgr1vtx  29393  cplgr0  29460  cplgr1v  29465  wwlksn0s  29894  clwwlkn  30058  clwwlkn1  30073  0ewlk  30146  1ewlk  30147  0wlk  30148  0conngr  30224  frgr0v  30294  frgr0  30297  frgr1v  30303  1vwmgr  30308  chocnul  31360  chnub  32984  locfinref  33787  esumnul  34012  derang0  35137  unt0  35673  fdc  37705  lub0N  39145  glb0N  39149  0psubN  39706  sticksstones11  42113  cantnfresb  43286  safesnsupfilb  43380  nla0002  43386  nla0003  43387  iso0  44276  fnchoice  44929  eliuniincex  45011  eliincex  45012  limcdm0  45539  2ffzoeq  47242  iccpartiltu  47296  iccpartigtl  47297  0mgm  47889  linds0  48194  0thincg  48717