Theorem ral0 4440

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1539  ∀wral 3063  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-ral 3068  df-dif 3886  df-nul 4254

This theorem is referenced by:  int0  4890  0iin  4989  po0  5511  so0  5530  mpt0  6559  ixp0x  8672  ac6sfi  8988  sup0riota  9154  infpssrlem4  9993  axdc3lem4  10140  0tsk  10442  uzsupss  12609  xrsupsslem  12970  xrinfmsslem  12971  xrsup0  12986  fsuppmapnn0fiubex  13640  swrd0  14299  swrdspsleq  14306  repswsymballbi  14421  cshw1  14463  rexfiuz  14987  lcmf0  16267  2prm  16325  0ssc  17468  0subcat  17469  drsdirfi  17938  0pos  17954  0posOLD  17955  mrelatglb0  18194  sgrp0b  18298  ga0  18819  psgnunilem3  19019  lbsexg  20341  ocv0  20794  mdetunilem9  21677  imasdsf1olem  23434  prdsxmslem2  23591  lebnumlem3  24032  cniccbdd  24530  ovolicc2lem4  24589  c1lip1  25066  ulm0  25455  istrkg2ld  26725  nbgr0vtx  27626  nbgr1vtx  27628  cplgr0  27695  cplgr1v  27700  wwlksn0s  28127  clwwlkn  28291  clwwlkn1  28306  0ewlk  28379  1ewlk  28380  0wlk  28381  0conngr  28457  frgr0v  28527  frgr0  28530  frgr1v  28536  1vwmgr  28541  chocnul  29591  locfinref  31693  esumnul  31916  derang0  33031  unt0  33552  naddid1  33763  fdc  35830  lub0N  37130  glb0N  37134  0psubN  37690  sticksstones11  40040  iso0  41814  fnchoice  42461  eliuniincex  42548  eliincex  42549  limcdm0  43049  2ffzoeq  44708  iccpartiltu  44762  iccpartigtl  44763  0mgm  45216  linds0  45694  0thincg  46219