Theorem rab0 4338

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 3400	. 2 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2		ab0 4332	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3		noel 4290	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
4	3	intnanr 487	. . 3 ⊢ ¬ (𝑥 ∈ ∅ ∧ 𝜑)
5	2, 4	mpgbir 1800	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
6	1, 5	eqtri 2759	1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Syntax hints:  ¬ wn 3   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714  {crab 3399  ∅c0 4285

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-dif 3904  df-nul 4286

This theorem is referenced by:  rabsnif  4680  fvmptrabfv  6973  supp0  8107  sup00  9368  scott0  9798  psgnfval  19429  pmtrsn  19448  rrgval  20630  00lsp  20932  leftval  27845  rightval  27846  uvtx0  29467  vtxdg0e  29548  wwlksn  29910  wspthsn  29921  iswwlksnon  29926  iswspthsnon  29929  clwwlk0on0  30167  fxpgaval  33249  zar0ring  34035  wevgblacfn  35303  satf0  35566  fvmptrab  47538  fvmptrabdm  47539  prprspr2  47764  initopropdlem  49485  termopropdlem  49486