Theorem rex0 4307

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2144  ∃wrex 3086  ∅c0 4278

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-dif 4047  df-nul 4279

This theorem is used by:  reu0  4308  rmo0  4309  rab0  4334  0iun  5020  0qs  8786  sup0riota  9461  cfeq0  10337  cfsuc  10338  hashge2el2difr  14629  cshws0  17284  addsrid  28355  muls01  28503  mulsrid  28504  elons2  28649  onaddscl  28668  onmulscl  28669  n0cut  28725  0ringirng  34367  dya2iocuni  34961  eulerpartlemgh  35056  pmapglb2xN  40922  elpadd0  40959  tfsconcatb0  44439  sprsymrelfvlem  48665  ipolub00  50200