Theorem rab0 4352

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 3409	. 2 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2		ab0 4346	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3		noel 4304	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
4	3	intnanr 487	. . 3 ⊢ ¬ (𝑥 ∈ ∅ ∧ 𝜑)
5	2, 4	mpgbir 1799	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
6	1, 5	eqtri 2753	1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2708  {crab 3408  ∅c0 4299

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-dif 3920  df-nul 4300

This theorem is referenced by:  rabsnif  4690  fvmptrabfv  7003  supp0  8147  sup00  9423  scott0  9846  psgnfval  19437  pmtrsn  19456  rrgval  20613  00lsp  20894  leftval  27778  rightval  27779  uvtx0  29328  vtxdg0e  29409  wwlksn  29774  wspthsn  29785  iswwlksnon  29790  iswspthsnon  29793  clwwlk0on0  30028  fxpgaval  33131  zar0ring  33875  wevgblacfn  35103  satf0  35366  fvmptrab  47297  fvmptrabdm  47298  prprspr2  47523  initopropdlem  49233  termopropdlem  49234