Theorem ral0 4396

Description: Vacuous universal quantification is always true. (Contributed by NM, 20-Oct-2005.) Avoid df-clel 2811, ax-8 2115. (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 4392	. 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑)
3	1, 2	ax-mp 5	1 ⊢ ∀𝑥 ∈ ∅ 𝜑

Syntax hints:   = wceq 1542  ∀wral 3053  ∅c0 4209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-ral 3058  df-dif 3844  df-nul 4210

This theorem is referenced by:  int0  4847  0iin  4946  po0  5454  so0  5473  mpt0  6473  ixp0x  8529  ac6sfi  8829  sup0riota  8995  infpssrlem4  9799  axdc3lem4  9946  0tsk  10248  uzsupss  12415  xrsupsslem  12776  xrinfmsslem  12777  xrsup0  12792  fsuppmapnn0fiubex  13444  swrd0  14102  swrdspsleq  14109  repswsymballbi  14224  cshw1  14266  rexfiuz  14790  lcmf0  16068  2prm  16126  0ssc  17205  0subcat  17206  drsdirfi  17657  0pos  17673  mrelatglb0  17904  sgrp0b  18018  ga0  18539  psgnunilem3  18735  lbsexg  20048  ocv0  20486  mdetunilem9  21364  imasdsf1olem  23119  prdsxmslem2  23275  lebnumlem3  23708  cniccbdd  24206  ovolicc2lem4  24265  c1lip1  24741  ulm0  25130  istrkg2ld  26398  nbgr0vtx  27290  nbgr1vtx  27292  cplgr0  27359  cplgr1v  27364  wwlksn0s  27791  clwwlkn  27955  clwwlkn1  27970  0ewlk  28043  1ewlk  28044  0wlk  28045  0conngr  28121  frgr0v  28191  frgr0  28194  frgr1v  28200  1vwmgr  28205  chocnul  29255  locfinref  31355  esumnul  31578  derang0  32694  unt0  33215  naddid1  33469  fdc  35515  lub0N  36815  glb0N  36819  0psubN  37375  iso0  41447  fnchoice  42094  eliuniincex  42181  eliincex  42182  limcdm0  42685  2ffzoeq  44338  iccpartiltu  44392  iccpartigtl  44393  0mgm  44846  linds0  45324  0thincg  45779