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

Theorem rab0 4343
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 3407 . 2 {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2 ab0 4335 . . 3 ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3 noel 4291 . . . 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 3406  c0 4283
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 3407  df-dif 3914  df-nul 4284
This theorem is referenced by:  rabsnif  4685  fvmptrabfv  6980  supp0  8098  sup00  9405  scott0  9827  psgnfval  19287  pmtrsn  19306  00lsp  20457  rrgval  20773  leftval  27215  rightval  27216  uvtx0  28384  vtxdg0e  28464  wwlksn  28824  wspthsn  28835  iswwlksnon  28840  iswspthsnon  28843  clwwlk0on0  29078  zar0ring  32516  satf0  34023  fvmptrab  45610  fvmptrabdm  45611  prprspr2  45796
  Copyright terms: Public domain W3C validator