Theorem ral0 4513

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1542  ∀wral 3062  ∅c0 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-ral 3063  df-dif 3952  df-nul 4324

This theorem is referenced by:  int0  4967  0iin  5068  po0  5606  so0  5625  mpt0  6693  naddrid  8682  ixp0x  8920  ac6sfi  9287  sup0riota  9460  infpssrlem4  10301  axdc3lem4  10448  0tsk  10750  uzsupss  12924  xrsupsslem  13286  xrinfmsslem  13287  xrsup0  13302  fsuppmapnn0fiubex  13957  swrd0  14608  swrdspsleq  14615  repswsymballbi  14730  cshw1  14772  rexfiuz  15294  lcmf0  16571  2prm  16629  0ssc  17787  0subcat  17788  drsdirfi  18258  0pos  18274  0posOLD  18275  mrelatglb0  18514  sgrp0b  18619  ga0  19162  psgnunilem3  19364  lbsexg  20777  ocv0  21230  mdetunilem9  22122  imasdsf1olem  23879  prdsxmslem2  24038  lebnumlem3  24479  cniccbdd  24978  ovolicc2lem4  25037  c1lip1  25514  ulm0  25903  precsexlem9  27661  istrkg2ld  27711  nbgr0vtx  28613  nbgr1vtx  28615  cplgr0  28682  cplgr1v  28687  wwlksn0s  29115  clwwlkn  29279  clwwlkn1  29294  0ewlk  29367  1ewlk  29368  0wlk  29369  0conngr  29445  frgr0v  29515  frgr0  29518  frgr1v  29524  1vwmgr  29529  chocnul  30581  locfinref  32821  esumnul  33046  derang0  34160  unt0  34680  fdc  36613  lub0N  38059  glb0N  38063  0psubN  38620  sticksstones11  40972  cantnfresb  42074  safesnsupfilb  42169  nla0002  42175  nla0003  42176  iso0  43066  fnchoice  43713  eliuniincex  43798  eliincex  43799  limcdm0  44334  2ffzoeq  46036  iccpartiltu  46090  iccpartigtl  46091  0mgm  46544  linds0  47146  0thincg  47670