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

Syntax hints:  ¬ wn 3   = wceq 1570  ∀wral 3079  ∃wrex 3089  {crab 3416  ∅c0 4286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-dif 3908  df-nul 4287

This theorem is referenced by:  rabsnif  4689  fvmptrabfv  7022  supp0  8157  sup00  9421  scott0  9856  psgnfval  19565  pmtrsn  19584  rrgval  20796  00lsp  21102  leftval  28042  rightval  28043  uvtx0  29744  vtxdg0e  29824  wwlksn  30186  wspthsn  30197  iswwlksnon  30202  iswspthsnon  30205  clwwlk0on0  30443  fxpgaval  33487  zar0ring  34268  wevgblacfn  35595  satf0  35864  fvmptrab  48029  fvmptrabdm  48030  prprspr2  48267  initopropdlem  50018  termopropdlem  50019