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

Theorem rab0 4341
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 3152 . 2 {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2 ab0 4337 . . 3 ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3 noel 4300 . . . 4 ¬ 𝑥 ∈ ∅
43intnanr 488 . . 3 ¬ (𝑥 ∈ ∅ ∧ 𝜑)
52, 4mpgbir 1793 . 2 {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
61, 5eqtri 2849 1 {𝑥 ∈ ∅ ∣ 𝜑} = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 396   = wceq 1530  wcel 2107  {cab 2804  {crab 3147  c0 4295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-dif 3943  df-nul 4296
This theorem is referenced by:  rabsnif  4658  fvmptrabfv  6797  supp0  7831  sup00  8922  scott0  9309  psgnfval  18564  pmtrsn  18583  00lsp  19689  rrgval  19995  uvtx0  27109  vtxdg0e  27189  wwlksn  27548  wspthsn  27559  iswwlksnon  27564  iswspthsnon  27567  clwwlk0on0  27804  satf0  32522  fvmptrab  43376  fvmptrabdm  43377  prprspr2  43531
  Copyright terms: Public domain W3C validator