Theorem rab0 4339

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.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Assertion

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

Proof of Theorem rab0

Step	Hyp	Ref	Expression
1		rex0 4313	. . . 4 ⊢ ¬ ∃𝑥 ∈ ∅ ¬ 𝜑
2		dfral2 3113	. . . 4 ⊢ (∀𝑥 ∈ ∅ 𝜑 ↔ ¬ ∃𝑥 ∈ ∅ ¬ 𝜑)
3	1, 2	mpbir 233	. . 3 ⊢ ∀𝑥 ∈ ∅ 𝜑
4	3	rspec 3253	. 2 ⊢ (𝑥 ∈ ∅ → 𝜑)
5	4	rabeqc 3426	1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Syntax hints:  ¬ wn 3   = wceq 1560  ∀wral 3076  ∃wrex 3086  {crab 3414  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-12 2212  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3077  df-rex 3087  df-rab 3415  df-dif 3907  df-nul 4286

This theorem is referenced by:  rabsnif  4682  fvmptrabfv  7008  supp0  8145  sup00  9411  scott0  9844  psgnfval  19540  pmtrsn  19559  rrgval  20743  00lsp  21045  leftval  27939  rightval  27940  uvtx0  29592  vtxdg0e  29672  wwlksn  30034  wspthsn  30045  iswwlksnon  30050  iswspthsnon  30053  clwwlk0on0  30291  fxpgaval  33344  zar0ring  34172  wevgblacfn  35451  satf0  35719  fvmptrab  47883  fvmptrabdm  47884  prprspr2  48121  initopropdlem  49858  termopropdlem  49859