Theorem ral0 4454

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

Assertion

Ref	Expression
ral0	⊢ ∀𝑥 ∈ ∅ 𝜑

Proof of Theorem ral0

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

This proof depends on syntax axioms:   = wceq 1570  ∀wral 3077  ∅c0 4279

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 2155  ax-ext 2733

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 2740  df-cleq 2753  df-ral 3078  df-dif 3902  df-nul 4280

This theorem is used by:  int0  4922  0iin  5022  po0  5576  so0  5597  mpt0  6679  naddrid  8686  ixp0x  8947  ac6sfi  9268  sup0riota  9451  infpssrlem4  10377  axdc3lem4  10524  0tsk  10833  uzsupss  13060  xrsupsslem  13430  xrinfmsslem  13431  xrsup0  13446  fsuppmapnn0fiubex  14128  swrd0  14801  swrdspsleq  14808  repswsymballbi  14924  cshw1  14966  rexfiuz  15508  lcmf0  16802  2prm  16860  0ssc  18005  0subcat  18006  drsdirfi  18472  0pos  18488  mrelatglb0  18728  s1chn  18787  chnub  18789  sgrp0b  18910  ga0  19505  psgnunilem3  19703  lbsexg  21435  ocv0  21976  mdetunilem9  22928  imasdsf1olem  24685  prdsxmslem2  24841  lebnumlem3  25277  cniccbdd  25775  ovolicc2lem4  25834  c1lip1  26310  ulm0  26711  rightge0  28200  precsexlem9  28594  onsbnd  28660  n0fincut  28734  zcuts  28786  twocut  28802  addhalfcut  28838  0reno  28875  istrkg2ld  28915  nbgr1vtx  29932  cplgr0  29999  cplgr1v  30004  wwlksn0s  30443  clwwlkn  30610  clwwlkn1  30625  0ewlk  30698  1ewlk  30699  0wlk  30700  0conngr  30786  frgr0v  30856  frgr0  30859  frgr1v  30865  1vwmgr  30870  chocnul  31923  locfinref  34466  esumnul  34673  derang0  35913  unt0  36455  nmulr0  36924  mh-inf3f1  37309  fdc  38659  lub0N  40226  glb0N  40230  0psubN  40786  sticksstones11  43186  cantnfresb  44310  safesnsupfilb  44403  nla0002  44409  nla0003  44410  iso0  45276  fnchoice  46015  eliuniincex  46093  eliincex  46094  limcdm0  46599  2ffzoeq  48367  iccpartiltu  48473  iccpartigtl  48474  0mgm  49232  linds0  49546  0funcALT  50165  0thincg  50535  termolmd  50747