Theorem rex0 4310

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

Syntax hints:  ¬ wn 3   ∈ wcel 2111  ∃wrex 3056  ∅c0 4283

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-dif 3905  df-nul 4284

This theorem is referenced by:  reu0  4311  rmo0  4312  0iun  5011  0qs  8687  sup0riota  9350  cfeq0  10144  cfsuc  10145  hashge2el2difr  14385  cshws0  17010  addsrid  27905  muls01  28049  mulsrid  28050  elons2  28193  onaddscl  28208  onmulscl  28209  n0scut  28260  1p1e2s  28337  0ringirng  33697  dya2iocuni  34291  eulerpartlemgh  34386  pmapglb2xN  39810  elpadd0  39847  tfsconcatb0  43376  sprsymrelfvlem  47520  ipolub00  49023