Theorem rab0 3909

Description: Any restricted class abstraction restricted to the empty set is empty. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) (Proof shortened by JJ, 14-Jul-2021.)

Assertion

Ref	Expression
rab0	⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Proof of Theorem rab0

Step	Hyp	Ref	Expression
1		df-rab 2905	. 2 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2		ab0 3905	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3		noel 3878	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
4	3	intnanr 952	. . 3 ⊢ ¬ (𝑥 ∈ ∅ ∧ 𝜑)
5	2, 4	mpgbir 1717	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
6	1, 5	eqtri 2632	1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Syntax hints:  ¬ wn 3   ∧ wa 383   = wceq 1475   ∈ wcel 1977  {cab 2596  {crab 2900  ∅c0 3874

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-nul 3875

This theorem is referenced by:  rabsnif  4202  supp0  7187  sup00  8253  scott0  8632  psgnfval  17743  pmtrsn  17762  00lsp  18802  rrgval  19108  usgra0v  25900  vdgr0  26427  uvtxa0  40620  vtxdg0e  40689  wwlksn  41040  wspthsn  41046  iswwlksnon  41051  iswspthsnon  41052  clwwlksn  41189