Theorem rex0 4311

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-dif 3905  df-nul 4283

This theorem is used by:  reu0  4312  rmo0  4313  rab0  4338  0iun  5025  0qs  8766  sup0riota  9440  cfeq0  10262  cfsuc  10263  hashge2el2difr  14550  cshws0  17199  addsrid  28237  muls01  28385  mulsrid  28386  elons2  28531  onaddscl  28550  onmulscl  28551  n0cut  28607  0ringirng  34207  dya2iocuni  34802  eulerpartlemgh  34897  pmapglb2xN  40653  elpadd0  40690  tfsconcatb0  44193  sprsymrelfvlem  48398  ipolub00  49927