Theorem ral0 4518

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

Syntax hints:   = wceq 1536  ∀wral 3058  ∅c0 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-ral 3059  df-dif 3965  df-nul 4339

This theorem is referenced by:  int0  4966  0iin  5068  po0  5613  so0  5633  mpt0  6710  naddrid  8719  ixp0x  8964  ac6sfi  9317  sup0riota  9502  infpssrlem4  10343  axdc3lem4  10490  0tsk  10792  uzsupss  12979  xrsupsslem  13345  xrinfmsslem  13346  xrsup0  13361  fsuppmapnn0fiubex  14029  swrd0  14692  swrdspsleq  14699  repswsymballbi  14814  cshw1  14856  rexfiuz  15382  lcmf0  16667  2prm  16725  0ssc  17887  0subcat  17888  drsdirfi  18362  0pos  18378  0posOLD  18379  mrelatglb0  18618  sgrp0b  18753  ga0  19328  psgnunilem3  19528  lbsexg  21183  ocv0  21712  mdetunilem9  22641  imasdsf1olem  24398  prdsxmslem2  24557  lebnumlem3  25008  cniccbdd  25509  ovolicc2lem4  25568  c1lip1  26050  ulm0  26448  precsexlem9  28253  zscut  28407  nohalf  28421  addhalfcut  28433  istrkg2ld  28482  nbgr1vtx  29389  cplgr0  29456  cplgr1v  29461  wwlksn0s  29890  clwwlkn  30054  clwwlkn1  30069  0ewlk  30142  1ewlk  30143  0wlk  30144  0conngr  30220  frgr0v  30290  frgr0  30293  frgr1v  30299  1vwmgr  30304  chocnul  31356  chnub  32985  locfinref  33801  esumnul  34028  derang0  35153  unt0  35690  fdc  37731  lub0N  39170  glb0N  39174  0psubN  39731  sticksstones11  42137  cantnfresb  43313  safesnsupfilb  43407  nla0002  43413  nla0003  43414  iso0  44302  fnchoice  44966  eliuniincex  45048  eliincex  45049  limcdm0  45573  2ffzoeq  47276  iccpartiltu  47346  iccpartigtl  47347  0mgm  48009  linds0  48310  0thincg  48850