Theorem rab0 4342

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570  ∀wral 3081  ∃wrex 3091  {crab 3418  ∅c0 4286

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 2148  ax-9 2156  ax-12 2216  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-dif 3909  df-nul 4287

This theorem is used by:  rabsnif  4691  fvmptrabfv  7026  supp0  8167  sup00  9432  scott0OLD  9874  psgnfval  19614  pmtrsn  19633  rrgval  20846  00lsp  21152  leftval  28093  rightval  28094  uvtx0  29802  vtxdg0e  29882  wwlksn  30253  wspthsn  30264  iswwlksnon  30269  iswspthsnon  30272  clwwlk0on0  30510  fxpgaval  33551  zar0ring  34332  wevgblacfn  35652  satf0  35901  fvmptrab  48087  fvmptrabdm  48088  prprspr2  48325  initopropdlem  50075  termopropdlem  50076