Theorem rab0 4349

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

Syntax hints:  ¬ wn 3   = wceq 1567  ∀wral 3085  ∃wrex 3095  {crab 3423  ∅c0 4294

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rex 3096  df-rab 3424  df-dif 3916  df-nul 4295

This theorem is referenced by:  rabsnif  4694  fvmptrabfv  7023  supp0  8160  sup00  9424  scott0  9859  psgnfval  19569  pmtrsn  19588  rrgval  20781  00lsp  21079  leftval  28007  rightval  28008  uvtx0  29684  vtxdg0e  29764  wwlksn  30126  wspthsn  30137  iswwlksnon  30142  iswspthsnon  30145  clwwlk0on0  30383  fxpgaval  33427  zar0ring  34212  wevgblacfn  35493  satf0  35762  fvmptrab  47917  fvmptrabdm  47918  prprspr2  48155  initopropdlem  49902  termopropdlem  49903