![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eq0rdv | Structured version Visualization version GIF version |
Description: Deduction rule 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 119 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝑥 ∈ ∅)) |
3 | 2 | ssrdv 3759 | . 2 ⊢ (𝜑 → 𝐴 ⊆ ∅) |
4 | ss0 4119 | . 2 ⊢ (𝐴 ⊆ ∅ → 𝐴 = ∅) | |
5 | 3, 4 | syl 17 | 1 ⊢ (𝜑 → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 = wceq 1631 ∈ wcel 2145 ⊆ wss 3724 ∅c0 4064 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-v 3353 df-dif 3727 df-in 3731 df-ss 3738 df-nul 4065 |
This theorem is referenced by: map0b 8050 disjen 8274 mapdom1 8282 pwxpndom2 9690 fzdisj 12576 smu01lem 15416 prmreclem5 15832 vdwap0 15888 natfval 16814 fucbas 16828 fuchom 16829 coafval 16922 efgval 18338 lsppratlem6 19368 lbsextlem4 19377 psrvscafval 19606 cfinufil 21953 ufinffr 21954 fin1aufil 21957 bldisj 22424 reconnlem1 22850 pcofval 23030 bcthlem5 23345 volfiniun 23536 fta1g 24148 fta1 24284 rpvmasum 25437 bj-projval 33316 finxpnom 33576 ipo0 39179 ifr0 39180 limclner 40402 |
Copyright terms: Public domain | W3C validator |