Theorem rex0 4335

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 4313	. . 3 ⊢ ¬ 𝑥 ∈ ∅
2	1	pm2.21i 119	. 2 ⊢ (𝑥 ∈ ∅ → ¬ 𝜑)
3	2	nrex 3064	1 ⊢ ¬ ∃𝑥 ∈ ∅ 𝜑

Syntax hints:  ¬ wn 3   ∈ wcel 2108  ∃wrex 3060  ∅c0 4308

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-8 2110  ax-9 2118  ax-ext 2707

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 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-dif 3929  df-nul 4309

This theorem is referenced by:  reu0  4336  rmo0  4337  0iun  5039  0qs  8781  sup0riota  9478  cfeq0  10270  cfsuc  10271  hashge2el2difr  14499  cshws0  17121  addsrid  27923  muls01  28067  mulsrid  28068  elons2  28211  onaddscl  28226  onmulscl  28227  n0scut  28278  1p1e2s  28354  0ringirng  33730  dya2iocuni  34315  eulerpartlemgh  34410  pmapglb2xN  39791  elpadd0  39828  tfsconcatb0  43368  sprsymrelfvlem  47504  ipolub00  48967