Theorem rex0 4288

Description: Vacuous restricted existential quantification is false. (Contributed by NM, 15-Oct-2003.)

Assertion

Ref	Expression
rex0	⊢ ¬ ∃𝑥 ∈ ∅ 𝜑

Proof of Theorem rex0

Step	Hyp	Ref	Expression
1		noel 4261	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 119	. 2 ⊢ (𝑥 ∈ ∅ → ¬ 𝜑)
3	2	nrex 3196	1 ⊢ ¬ ∃𝑥 ∈ ∅ 𝜑

Syntax hints:  ¬ wn 3   ∈ wcel 2108  ∃wrex 3064  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-dif 3886  df-nul 4254

This theorem is referenced by:  reu0  4289  rmo0  4290  0iun  4988  sup0riota  9154  cfeq0  9943  cfsuc  9944  hashge2el2difr  14123  cshws0  16731  dya2iocuni  32150  eulerpartlemgh  32245  addsid1  34054  0qs  36427  pmapglb2xN  37713  elpadd0  37750  sprsymrelfvlem  44830  ipolub00  46167