Theorem rab0 4314

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 3392	. 2 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2		ab0 4308	. . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3		noel 4266	. . . 4 ⊢ ¬ 𝑥 ∈ ∅
4	3	intnanr 488	. . 3 ⊢ ¬ (𝑥 ∈ ∅ ∧ 𝜑)
5	2, 4	mpgbir 1806	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
6	1, 5	eqtri 2762	1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅

Syntax hints:  ¬ wn 3   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2717  {crab 3391  ∅c0 4261

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-dif 3886  df-nul 4262

This theorem is referenced by:  rabsnif  4655  fvmptrabfv  6968  supp0  8105  sup00  9368  scott0  9801  psgnfval  19466  pmtrsn  19485  rrgval  20669  00lsp  20971  leftval  27859  rightval  27860  uvtx0  29481  vtxdg0e  29561  wwlksn  29923  wspthsn  29934  iswwlksnon  29939  iswspthsnon  29942  clwwlk0on0  30180  fxpgaval  33248  zar0ring  34062  wevgblacfn  35337  satf0  35600  fvmptrab  47755  fvmptrabdm  47756  prprspr2  47993  initopropdlem  49730  termopropdlem  49731