MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rab0 Structured version   Visualization version   GIF version

Theorem rab0 4383
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
StepHypRef Expression
1 df-rab 3434 . 2 {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2 ab0 4375 . . 3 ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3 noel 4331 . . . 4 ¬ 𝑥 ∈ ∅
43intnanr 489 . . 3 ¬ (𝑥 ∈ ∅ ∧ 𝜑)
52, 4mpgbir 1802 . 2 {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
61, 5eqtri 2761 1 {𝑥 ∈ ∅ ∣ 𝜑} = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 397   = wceq 1542  wcel 2107  {cab 2710  {crab 3433  c0 4323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-dif 3952  df-nul 4324
This theorem is referenced by:  rabsnif  4728  fvmptrabfv  7030  supp0  8151  sup00  9459  scott0  9881  psgnfval  19368  pmtrsn  19387  00lsp  20592  rrgval  20903  leftval  27358  rightval  27359  uvtx0  28651  vtxdg0e  28731  wwlksn  29091  wspthsn  29102  iswwlksnon  29107  iswspthsnon  29110  clwwlk0on0  29345  zar0ring  32858  satf0  34363  fvmptrab  46000  fvmptrabdm  46001  prprspr2  46186
  Copyright terms: Public domain W3C validator