Theorem rex0 4308

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2145  ∃wrex 3087  ∅c0 4279

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-dif 3902  df-nul 4280

This theorem is used by:  reu0  4309  rmo0  4310  rab0  4335  0iun  5021  0qs  8767  sup0riota  9442  cfeq0  10315  cfsuc  10316  hashge2el2difr  14606  cshws0  17259  addsrid  28332  muls01  28480  mulsrid  28481  elons2  28626  onaddscl  28645  onmulscl  28646  n0cut  28702  0ringirng  34303  dya2iocuni  34898  eulerpartlemgh  34993  pmapglb2xN  40797  elpadd0  40834  tfsconcatb0  44304  sprsymrelfvlem  48516  ipolub00  50045