| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rab0 | Structured version Visualization version GIF version | ||
| 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.) |
| Ref | Expression |
|---|---|
| rab0 | ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-rab 3437 | . 2 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} | |
| 2 | ab0 4380 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑)) | |
| 3 | noel 4338 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
| 4 | 3 | intnanr 487 | . . 3 ⊢ ¬ (𝑥 ∈ ∅ ∧ 𝜑) |
| 5 | 2, 4 | mpgbir 1799 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ |
| 6 | 1, 5 | eqtri 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 |