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

Theorem rab0 4156
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 3098 . 2 {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2 ab0 4152 . . 3 ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3 noel 4119 . . . 4 ¬ 𝑥 ∈ ∅
43intnanr 482 . . 3 ¬ (𝑥 ∈ ∅ ∧ 𝜑)
52, 4mpgbir 1895 . 2 {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
61, 5eqtri 2821 1 {𝑥 ∈ ∅ ∣ 𝜑} = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 385   = wceq 1653  wcel 2157  {cab 2785  {crab 3093  c0 4115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-nul 4116
This theorem is referenced by:  rabsnif  4447  fvmptrabfv  6534  supp0  7537  sup00  8612  scott0  8999  psgnfval  18233  pmtrsn  18252  00lsp  19302  rrgval  19610  uvtx0  26640  vtxdg0e  26724  wwlksn  27088  wspthsn  27100  iswwlksnon  27105  iswwlksnonOLD  27106  iswspthsnon  27109  iswspthsnonOLD  27110  clwwlknOLD  27331  clwwlk0on0  27430  fvmptrab  42147  fvmptrabdm  42148
  Copyright terms: Public domain W3C validator