Theorem rab0 4335

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 4308	. . . 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 1570  ∀wral 3076  ∃wrex 3086  {crab 3412  ∅c0 4279

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-12 2213  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-dif 3902  df-nul 4280

This theorem is used by:  rabsnif  4684  fvmptrabfv  7019  supp0  8163  sup00  9435  scott0OLD  9877  psgnfval  19627  pmtrsn  19646  rrgval  20859  00lsp  21165  leftval  28114  rightval  28115  uvtx0  29854  vtxdg0e  29934  wwlksn  30305  wspthsn  30316  iswwlksnon  30321  iswspthsnon  30324  clwwlk0on0  30562  fxpgaval  33607  zar0ring  34388  wevgblacfn  35708  satf0  35951  fvmptrab  48180  fvmptrabdm  48181  prprspr2  48418  initopropdlem  50166  termopropdlem  50167