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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570  ∀wral 3077  ∃wrex 3087  {crab 3413  ∅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 2733

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 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-dif 3902  df-nul 4280

This theorem is used by:  rabsnif  4684  fvmptrabfv  7024  supp0  8175  sup00  9450  scott0OLD  9931  psgnfval  19707  pmtrsn  19726  rrgval  20942  00lsp  21249  leftval  28228  rightval  28229  uvtx0  29968  vtxdg0e  30048  wwlksn  30419  wspthsn  30430  iswwlksnon  30435  iswspthsnon  30438  clwwlk0on0  30676  fxpgaval  33721  zar0ring  34503  wevgblacfn  35873  satf0  36116  fvmptrab  48331  fvmptrabdm  48332  prprspr2  48569  initopropdlem  50317  termopropdlem  50318