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

Theorem rab0 4386
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 3437 . 2 {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)}
2 ab0 4380 . . 3 ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑))
3 noel 4338 . . . 4 ¬ 𝑥 ∈ ∅
43intnanr 487 . . 3 ¬ (𝑥 ∈ ∅ ∧ 𝜑)
52, 4mpgbir 1799 . 2 {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅
61, 5eqtri 2765 1 {𝑥 ∈ ∅ ∣ 𝜑} = ∅
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395   = wceq 1540  wcel 2108  {cab 2714  {crab 3436  c0 4333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-dif 3954  df-nul 4334
This theorem is referenced by:  rabsnif  4723  fvmptrabfv  7048  supp0  8190  sup00  9504  scott0  9926  psgnfval  19518  pmtrsn  19537  rrgval  20697  00lsp  20979  leftval  27902  rightval  27903  uvtx0  29411  vtxdg0e  29492  wwlksn  29857  wspthsn  29868  iswwlksnon  29873  iswspthsnon  29876  clwwlk0on0  30111  zar0ring  33877  wevgblacfn  35114  satf0  35377  fvmptrab  47304  fvmptrabdm  47305  prprspr2  47505
  Copyright terms: Public domain W3C validator