Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ral0 | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ral0 | ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . 2 ⊢ ∅ = ∅ | |
2 | rzal 4392 | . 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |