Theorem rex0 4383

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

Syntax hints:  ¬ wn 3   ∈ wcel 2108  ∃wrex 3076  ∅c0 4352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-dif 3979  df-nul 4353

This theorem is referenced by:  reu0  4384  rmo0  4385  0iun  5086  0qs  8825  sup0riota  9534  cfeq0  10325  cfsuc  10326  hashge2el2difr  14530  cshws0  17149  addsrid  28015  muls01  28156  mulsrid  28157  elons2  28299  onaddscl  28304  onmulscl  28305  n0scut  28356  1p1e2s  28418  0ringirng  33689  dya2iocuni  34248  eulerpartlemgh  34343  pmapglb2xN  39729  elpadd0  39766  tfsconcatb0  43306  sprsymrelfvlem  47364  ipolub00  48665