Theorem ral0 4461

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

This proof depends on syntax axioms:   = wceq 1570  ∀wral 3081  ∅c0 4286

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-ral 3082  df-dif 3909  df-nul 4287

This theorem is used by:  int0  4929  0iin  5030  po0  5588  so0  5609  mpt0  6681  naddrid  8676  ixp0x  8930  ac6sfi  9251  sup0riota  9433  infpssrlem4  10305  axdc3lem4  10452  0tsk  10755  uzsupss  12980  xrsupsslem  13349  xrinfmsslem  13350  xrsup0  13365  fsuppmapnn0fiubex  14046  swrd0  14718  swrdspsleq  14725  repswsymballbi  14841  cshw1  14883  rexfiuz  15423  lcmf0  16714  2prm  16772  0ssc  17916  0subcat  17917  drsdirfi  18383  0pos  18399  mrelatglb0  18639  s1chn  18698  chnub  18700  sgrp0b  18818  ga0  19412  psgnunilem3  19610  lbsexg  21338  ocv0  21877  mdetunilem9  22827  imasdsf1olem  24581  prdsxmslem2  24737  lebnumlem3  25173  cniccbdd  25671  ovolicc2lem4  25730  c1lip1  26207  ulm0  26605  rightge0  28065  precsexlem9  28459  onsbnd  28525  n0fincut  28599  zcuts  28651  twocut  28667  addhalfcut  28703  0reno  28740  istrkg2ld  28780  nbgr1vtx  29766  cplgr0  29833  cplgr1v  29838  wwlksn0s  30277  clwwlkn  30444  clwwlkn1  30459  0ewlk  30532  1ewlk  30533  0wlk  30534  0conngr  30614  frgr0v  30684  frgr0  30687  frgr1v  30693  1vwmgr  30698  chocnul  31751  locfinref  34295  esumnul  34502  derang0  35698  unt0  36240  nmulr0  36724  fdc  38454  lub0N  40021  glb0N  40025  0psubN  40581  sticksstones11  42981  cantnfresb  44109  safesnsupfilb  44202  nla0002  44208  nla0003  44209  iso0  45075  fnchoice  45807  eliuniincex  45885  eliincex  45886  limcdm0  46392  2ffzoeq  48123  iccpartiltu  48229  iccpartigtl  48230  0mgm  48988  linds0  49302  0funcALT  49923  0thincg  50293  termolmd  50505