Theorem rex0 4300

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

Syntax hints:  ¬ wn 3   ∈ wcel 2114  ∃wrex 3061  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-dif 3892  df-nul 4274

This theorem is referenced by:  reu0  4301  rmo0  4302  0iun  5005  0qs  8709  sup0riota  9379  cfeq0  10178  cfsuc  10179  hashge2el2difr  14443  cshws0  17072  addsrid  27956  muls01  28104  mulsrid  28105  elons2  28250  onaddscl  28269  onmulscl  28270  n0cut  28326  0ringirng  33833  dya2iocuni  34427  eulerpartlemgh  34522  pmapglb2xN  40218  elpadd0  40255  tfsconcatb0  43772  sprsymrelfvlem  47950  ipolub00  49468