Theorem rex0 4318

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

This proof depends on syntax axioms:  ¬ wn 3   ∈ wcel 2146  ∃wrex 3092  ∅c0 4289

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-dif 3911  df-nul 4290

This theorem is used by:  reu0  4319  rmo0  4320  rab0  4345  0iun  5032  0qs  8769  sup0riota  9436  cfeq0  10258  cfsuc  10259  hashge2el2difr  14538  cshws0  17186  addsrid  28194  muls01  28342  mulsrid  28343  elons2  28488  onaddscl  28507  onmulscl  28508  n0cut  28564  0ringirng  34110  dya2iocuni  34704  eulerpartlemgh  34799  pmapglb2xN  40586  elpadd0  40623  tfsconcatb0  44111  sprsymrelfvlem  48279  ipolub00  49811