Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eq0rdv | Structured version Visualization version GIF version |
Description: Deduction for equality to the empty set. (Contributed by NM, 11-Jul-2014.) |
Ref | Expression |
---|---|
eq0rdv.1 | ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) |
Ref | Expression |
---|---|
eq0rdv | ⊢ (𝜑 → 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eq0rdv.1 | . . . 4 ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) | |
2 | 1 | pm2.21d 121 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∅)) |
3 | 2 | ssrdv 3970 | . 2 ⊢ (𝜑 → 𝐴 ⊆ ∅) |
4 | ss0 4349 | . 2 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | |
5 | 3, 4 | syl 17 | 1 ⊢ (𝜑 → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1528 ∈ wcel 2105 ⊆ wss 3933 ∅c0 4288 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-dif 3936 df-in 3940 df-ss 3949 df-nul 4289 |
This theorem is referenced by: map0b 8436 disjen 8662 mapdom1 8670 pwxpndom2 10075 fzdisj 12922 smu01lem 15822 prmreclem5 16244 vdwap0 16300 natfval 17204 fucbas 17218 fuchom 17219 coafval 17312 efgval 18772 lsppratlem6 19853 lbsextlem4 19862 psrvscafval 20098 cfinufil 22464 ufinffr 22465 fin1aufil 22468 bldisj 22935 reconnlem1 23361 pcofval 23541 bcthlem5 23858 volfiniun 24075 fta1g 24688 fta1 24824 rpvmasum 26029 unblimceq0 33743 bj-projval 34205 finxpnom 34564 ipo0 40658 ifr0 40659 limclner 41808 |
Copyright terms: Public domain | W3C validator |