Theorem ral0 4453

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1542  ∀wral 3052  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-ral 3053  df-dif 3906  df-nul 4288

This theorem is referenced by:  int0  4919  0iin  5021  po0  5557  so0  5578  mpt0  6642  naddrid  8621  ixp0x  8876  ac6sfi  9196  sup0riota  9381  infpssrlem4  10228  axdc3lem4  10375  0tsk  10678  uzsupss  12865  xrsupsslem  13234  xrinfmsslem  13235  xrsup0  13250  fsuppmapnn0fiubex  13927  swrd0  14594  swrdspsleq  14601  repswsymballbi  14715  cshw1  14757  rexfiuz  15283  lcmf0  16573  2prm  16631  0ssc  17773  0subcat  17774  drsdirfi  18240  0pos  18256  mrelatglb0  18496  s1chn  18555  chnub  18557  sgrp0b  18665  ga0  19239  psgnunilem3  19437  lbsexg  21131  ocv0  21644  mdetunilem9  22576  imasdsf1olem  24329  prdsxmslem2  24485  lebnumlem3  24930  cniccbdd  25430  ovolicc2lem4  25489  c1lip1  25970  ulm0  26368  rightge0  27829  precsexlem9  28223  onsbnd  28289  n0fincut  28363  zcuts  28415  twocut  28431  addhalfcut  28467  0reno  28504  istrkg2ld  28544  nbgr1vtx  29443  cplgr0  29510  cplgr1v  29515  wwlksn0s  29946  clwwlkn  30113  clwwlkn1  30128  0ewlk  30201  1ewlk  30202  0wlk  30203  0conngr  30279  frgr0v  30349  frgr0  30352  frgr1v  30358  1vwmgr  30363  chocnul  31416  locfinref  34019  esumnul  34226  derang0  35385  unt0  35927  fdc  37996  lub0N  39565  glb0N  39569  0psubN  40125  sticksstones11  42526  cantnfresb  43681  safesnsupfilb  43774  nla0002  43780  nla0003  43781  iso0  44663  fnchoice  45389  eliuniincex  45468  eliincex  45469  limcdm0  45978  2ffzoeq  47687  iccpartiltu  47782  iccpartigtl  47783  0mgm  48526  linds0  48825  0funcALT  49447  0thincg  49817  termolmd  50029