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 2817, ax-8 2109. (Revised by Gino Giotto, 2-Sep-2024.) |
Ref | Expression |
---|---|
ral0 | ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2739 | . 2 ⊢ ∅ = ∅ | |
2 | rzal 4440 | . 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ ∀𝑥 ∈ ∅ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∀wral 3065 ∅c0 4257 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2069 df-clab 2717 df-cleq 2731 df-ral 3070 df-dif 3891 df-nul 4258 |
This theorem is referenced by: int0 4894 0iin 4994 po0 5521 so0 5540 mpt0 6584 ixp0x 8723 ac6sfi 9067 sup0riota 9233 infpssrlem4 10071 axdc3lem4 10218 0tsk 10520 uzsupss 12689 xrsupsslem 13050 xrinfmsslem 13051 xrsup0 13066 fsuppmapnn0fiubex 13721 swrd0 14380 swrdspsleq 14387 repswsymballbi 14502 cshw1 14544 rexfiuz 15068 lcmf0 16348 2prm 16406 0ssc 17561 0subcat 17562 drsdirfi 18032 0pos 18048 0posOLD 18049 mrelatglb0 18288 sgrp0b 18392 ga0 18913 psgnunilem3 19113 lbsexg 20435 ocv0 20891 mdetunilem9 21778 imasdsf1olem 23535 prdsxmslem2 23694 lebnumlem3 24135 cniccbdd 24634 ovolicc2lem4 24693 c1lip1 25170 ulm0 25559 istrkg2ld 26830 nbgr0vtx 27732 nbgr1vtx 27734 cplgr0 27801 cplgr1v 27806 wwlksn0s 28235 clwwlkn 28399 clwwlkn1 28414 0ewlk 28487 1ewlk 28488 0wlk 28489 0conngr 28565 frgr0v 28635 frgr0 28638 frgr1v 28644 1vwmgr 28649 chocnul 29699 locfinref 31800 esumnul 32025 derang0 33140 unt0 33661 naddid1 33845 fdc 35912 lub0N 37210 glb0N 37214 0psubN 37770 sticksstones11 40119 iso0 41932 fnchoice 42579 eliuniincex 42666 eliincex 42667 limcdm0 43166 2ffzoeq 44831 iccpartiltu 44885 iccpartigtl 44886 0mgm 45339 linds0 45817 0thincg 46342 |
Copyright terms: Public domain | W3C validator |