![]() |
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 2809, ax-8 2108. (Revised by Gino Giotto, 2-Sep-2024.) |
Ref | Expression |
---|---|
ral0 | ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2731 | . 2 ⊢ ∅ = ∅ | |
2 | rzal 4502 | . 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∀wral 3060 ∅c0 4318 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-ral 3061 df-dif 3947 df-nul 4319 |
This theorem is referenced by: int0 4959 0iin 5060 po0 5598 so0 5617 mpt0 6679 naddrid 8665 ixp0x 8903 ac6sfi 9270 sup0riota 9442 infpssrlem4 10283 axdc3lem4 10430 0tsk 10732 uzsupss 12906 xrsupsslem 13268 xrinfmsslem 13269 xrsup0 13284 fsuppmapnn0fiubex 13939 swrd0 14590 swrdspsleq 14597 repswsymballbi 14712 cshw1 14754 rexfiuz 15276 lcmf0 16553 2prm 16611 0ssc 17769 0subcat 17770 drsdirfi 18240 0pos 18256 0posOLD 18257 mrelatglb0 18496 sgrp0b 18600 ga0 19128 psgnunilem3 19328 lbsexg 20726 ocv0 21163 mdetunilem9 22051 imasdsf1olem 23808 prdsxmslem2 23967 lebnumlem3 24408 cniccbdd 24907 ovolicc2lem4 24966 c1lip1 25443 ulm0 25832 istrkg2ld 27576 nbgr0vtx 28478 nbgr1vtx 28480 cplgr0 28547 cplgr1v 28552 wwlksn0s 28980 clwwlkn 29144 clwwlkn1 29159 0ewlk 29232 1ewlk 29233 0wlk 29234 0conngr 29310 frgr0v 29380 frgr0 29383 frgr1v 29389 1vwmgr 29394 chocnul 30444 locfinref 32652 esumnul 32877 derang0 33991 unt0 34510 fdc 36418 lub0N 37864 glb0N 37868 0psubN 38425 sticksstones11 40777 cantnfresb 41845 safesnsupfilb 41940 nla0002 41946 nla0003 41947 iso0 42837 fnchoice 43484 eliuniincex 43569 eliincex 43570 limcdm0 44107 2ffzoeq 45808 iccpartiltu 45862 iccpartigtl 45863 0mgm 46316 linds0 46794 0thincg 47318 |
Copyright terms: Public domain | W3C validator |