Theorem rex0 4326

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

Syntax hints:  ¬ wn 3   ∈ wcel 2109  ∃wrex 3054  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-dif 3920  df-nul 4300

This theorem is referenced by:  reu0  4327  rmo0  4328  0iun  5030  0qs  8739  sup0riota  9424  cfeq0  10216  cfsuc  10217  hashge2el2difr  14453  cshws0  17079  addsrid  27878  muls01  28022  mulsrid  28023  elons2  28166  onaddscl  28181  onmulscl  28182  n0scut  28233  1p1e2s  28309  0ringirng  33691  dya2iocuni  34281  eulerpartlemgh  34376  pmapglb2xN  39773  elpadd0  39810  tfsconcatb0  43340  sprsymrelfvlem  47495  ipolub00  48985