Theorem rex0 4313

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109  ∃wrex 3053  ∅c0 4286

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-dif 3908  df-nul 4287

This theorem is referenced by:  reu0  4314  rmo0  4315  0iun  5015  0qs  8697  sup0riota  9375  cfeq0  10169  cfsuc  10170  hashge2el2difr  14406  cshws0  17031  addsrid  27894  muls01  28038  mulsrid  28039  elons2  28182  onaddscl  28197  onmulscl  28198  n0scut  28249  1p1e2s  28326  0ringirng  33660  dya2iocuni  34250  eulerpartlemgh  34345  pmapglb2xN  39751  elpadd0  39788  tfsconcatb0  43317  sprsymrelfvlem  47475  ipolub00  48978