Theorem rab0 4313

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.)

Assertion

Ref	Expression
rab0	⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Proof of Theorem rab0

Step	Hyp	Ref	Expression
1		df-rab 3072	. 2 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2		ab0 4305	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3		noel 4261	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
4	3	intnanr 487	. . 3 ⊢ ¬ (𝑥 ∈ ∅ ∧ 𝜑)
5	2, 4	mpgbir 1803	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
6	1, 5	eqtri 2766	1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1539   ∈ wcel 2108  {cab 2715  {crab 3067  ∅c0 4253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-dif 3886  df-nul 4254

This theorem is referenced by:  rabsnif  4656  fvmptrabfv  6888  supp0  7953  sup00  9153  scott0  9575  psgnfval  19023  pmtrsn  19042  00lsp  20158  rrgval  20471  uvtx0  27664  vtxdg0e  27744  wwlksn  28103  wspthsn  28114  iswwlksnon  28119  iswspthsnon  28122  clwwlk0on0  28357  zar0ring  31730  satf0  33234  leftval  33974  rightval  33975  fvmptrab  44671  fvmptrabdm  44672  prprspr2  44858