Theorem rex0 4316

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

Syntax hints:  ¬ wn 3   ∈ wcel 2143  ∃wrex 3089  ∅c0 4287

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-dif 3909  df-nul 4288

This theorem is referenced by:  reu0  4317  rmo0  4318  rab0  4343  0iun  5028  0qs  8761  sup0riota  9427  cfeq0  10241  cfsuc  10242  hashge2el2difr  14520  cshws0  17162  addsrid  28135  muls01  28283  mulsrid  28284  elons2  28429  onaddscl  28448  onmulscl  28449  n0cut  28505  0ringirng  34057  dya2iocuni  34651  eulerpartlemgh  34746  pmapglb2xN  40524  elpadd0  40561  tfsconcatb0  44051  sprsymrelfvlem  48216  ipolub00  49748