Theorem rex0 4309

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

Syntax hints:  ¬ wn 3   ∈ wcel 2113  ∃wrex 3057  ∅c0 4282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-dif 3901  df-nul 4283

This theorem is referenced by:  reu0  4310  rmo0  4311  0iun  5013  0qs  8693  sup0riota  9357  cfeq0  10154  cfsuc  10155  hashge2el2difr  14390  cshws0  17015  addsrid  27908  muls01  28052  mulsrid  28053  elons2  28196  onaddscl  28211  onmulscl  28212  n0scut  28263  1p1e2s  28340  0ringirng  33723  dya2iocuni  34317  eulerpartlemgh  34412  pmapglb2xN  39891  elpadd0  39928  tfsconcatb0  43461  sprsymrelfvlem  47614  ipolub00  49117