Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rex0 | Structured version Visualization version GIF version |
Description: Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.) |
Ref | Expression |
---|---|
rex0 | ⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | noel 4245 | . . 3 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | pm2.21i 119 | . 2 ⊢ (𝑥 ∈ ∅ → ¬ 𝜑) |
3 | 2 | nrex 3188 | 1 ⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2110 ∃wrex 3062 ∅c0 4237 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3066 df-rex 3067 df-dif 3869 df-nul 4238 |
This theorem is referenced by: reu0 4273 rmo0 4274 0iun 4971 sup0riota 9081 cfeq0 9870 cfsuc 9871 hashge2el2difr 14047 cshws0 16655 dya2iocuni 31962 eulerpartlemgh 32057 addsid1 33864 0qs 36237 pmapglb2xN 37523 elpadd0 37560 sprsymrelfvlem 44615 ipolub00 45952 |
Copyright terms: Public domain | W3C validator |