Theorem rex0 4295

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

Syntax hints:  ¬ wn 3   ∈ wcel 2119  ∃wrex 3064  ∅c0 4268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-dif 3893  df-nul 4269

This theorem is referenced by:  reu0  4296  rmo0  4297  0iun  4999  0qs  8706  sup0riota  9376  cfeq0  10176  cfsuc  10177  hashge2el2difr  14441  cshws0  17070  addsrid  27981  muls01  28129  mulsrid  28130  elons2  28275  onaddscl  28294  onmulscl  28295  n0cut  28351  0ringirng  33880  dya2iocuni  34474  eulerpartlemgh  34569  pmapglb2xN  40271  elpadd0  40308  tfsconcatb0  43796  sprsymrelfvlem  47972  ipolub00  49490