Theorem rab0 4334

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 4307	. . . 4 ⊢ ¬ ∃𝑥 ∈ ∅ ¬ 𝜑
2		dfral2 3113	. . . 4 ⊢ (∀𝑥 ∈ ∅ 𝜑 ↔ ¬ ∃𝑥 ∈ ∅ ¬ 𝜑)
3	1, 2	mpbir 234	. . 3 ⊢ ∀𝑥 ∈ ∅ 𝜑
4	3	rspec 3253	. 2 ⊢ (𝑥 ∈ ∅ → 𝜑)
5	4	rabeqc 3424	1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569  ∀wral 3076  ∃wrex 3086  {crab 3412  ∅c0 4277

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-dif 4046  df-nul 4278

This theorem is used by:  rabsnif  4680  fvmptrabfv  7031  supp0  8189  sup00  9464  scott0OLD  9945  psgnfval  19723  pmtrsn  19742  rrgval  20958  00lsp  21265  leftval  28244  rightval  28245  uvtx0  29984  vtxdg0e  30064  wwlksn  30435  wspthsn  30446  iswwlksnon  30451  iswspthsnon  30454  clwwlk0on0  30692  fxpgaval  33778  zar0ring  34560  wevgblacfn  35962  satf0  36227  fvmptrab  48470  fvmptrabdm  48471  prprspr2  48708  initopropdlem  50470  termopropdlem  50471