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 3147 | . 2 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} | |
2 | ab0 4332 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ ↔ ∀𝑥 ¬ (𝑥 ∈ ∅ ∧ 𝜑)) | |
3 | noel 4295 | . . . 4 ⊢ ¬ 𝑥 ∈ ∅ | |
4 | 3 | intnanr 490 | . . 3 ⊢ ¬ (𝑥 ∈ ∅ ∧ 𝜑) |
5 | 2, 4 | mpgbir 1796 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ ∅ ∧ 𝜑)} = ∅ |
6 | 1, 5 | eqtri 2844 | 1 ⊢ {𝑥 ∈ ∅ ∣ 𝜑} = ∅ |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∧ wa 398 = wceq 1533 ∈ wcel 2110 {cab 2799 {crab 3142 ∅c0 4290 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-dif 3938 df-nul 4291 |
This theorem is referenced by: rabsnif 4652 fvmptrabfv 6793 supp0 7829 sup00 8922 scott0 9309 psgnfval 18622 pmtrsn 18641 00lsp 19747 rrgval 20054 uvtx0 27170 vtxdg0e 27250 wwlksn 27609 wspthsn 27620 iswwlksnon 27625 iswspthsnon 27628 clwwlk0on0 27865 satf0 32614 fvmptrab 43485 fvmptrabdm 43486 prprspr2 43674 |
Copyright terms: Public domain | W3C validator |