![]() |
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 4289 | . . 3 ⊢ ¬ 𝑥 ∈ ∅ | |
2 | 1 | pm2.21i 119 | . 2 ⊢ (𝑥 ∈ ∅ → ¬ 𝜑) |
3 | 2 | nrex 3076 | 1 ⊢ ¬ ∃𝑥 ∈ ∅ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∈ wcel 2107 ∃wrex 3072 ∅c0 4281 |
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-8 2109 ax-9 2117 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-ral 3064 df-rex 3073 df-dif 3912 df-nul 4282 |
This theorem is referenced by: reu0 4317 rmo0 4318 0iun 5022 sup0riota 9360 cfeq0 10151 cfsuc 10152 hashge2el2difr 14334 cshws0 16934 dya2iocuni 32687 eulerpartlemgh 32782 addsid1 34273 0qs 36763 pmapglb2xN 38167 elpadd0 38204 sprsymrelfvlem 45577 ipolub00 46913 |
Copyright terms: Public domain | W3C validator |