| 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 2816, ax-8 2110. (Revised by GG, 2-Sep-2024.) |
| Ref | Expression |
|---|---|
| ral0 | ⊢ ∀𝑥 ∈ ∅ 𝜑 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2737 | . 2 ⊢ ∅ = ∅ | |
| 2 | rzal 4509 | . 2 ⊢ (∅ = ∅ → ∀𝑥 ∈ ∅ 𝜑) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ ∀𝑥 ∈ ∅ 𝜑 |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∀wral 3061 ∅c0 4333 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-ral 3062 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: int0 4962 0iin 5064 po0 5609 so0 5630 mpt0 6710 naddrid 8721 ixp0x 8966 ac6sfi 9320 sup0riota 9505 infpssrlem4 10346 axdc3lem4 10493 0tsk 10795 uzsupss 12982 xrsupsslem 13349 xrinfmsslem 13350 xrsup0 13365 fsuppmapnn0fiubex 14033 swrd0 14696 swrdspsleq 14703 repswsymballbi 14818 cshw1 14860 rexfiuz 15386 lcmf0 16671 2prm 16729 0ssc 17882 0subcat 17883 drsdirfi 18351 0pos 18367 mrelatglb0 18606 sgrp0b 18741 ga0 19316 psgnunilem3 19514 lbsexg 21166 ocv0 21695 mdetunilem9 22626 imasdsf1olem 24383 prdsxmslem2 24542 lebnumlem3 24995 cniccbdd 25496 ovolicc2lem4 25555 c1lip1 26036 ulm0 26434 precsexlem9 28239 zscut 28393 nohalf 28407 addhalfcut 28419 istrkg2ld 28468 nbgr1vtx 29375 cplgr0 29442 cplgr1v 29447 wwlksn0s 29881 clwwlkn 30045 clwwlkn1 30060 0ewlk 30133 1ewlk 30134 0wlk 30135 0conngr 30211 frgr0v 30281 frgr0 30284 frgr1v 30290 1vwmgr 30295 chocnul 31347 s1chn 33000 chnub 33002 locfinref 33840 esumnul 34049 derang0 35174 unt0 35711 fdc 37752 lub0N 39190 glb0N 39194 0psubN 39751 sticksstones11 42157 cantnfresb 43337 safesnsupfilb 43431 nla0002 43437 nla0003 43438 iso0 44326 fnchoice 45034 eliuniincex 45114 eliincex 45115 limcdm0 45633 2ffzoeq 47339 iccpartiltu 47409 iccpartigtl 47410 0mgm 48082 linds0 48382 0funcALT 48921 0thincg 49107 |
| Copyright terms: Public domain | W3C validator |