![]() |
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.) Avoid ax-8 2109, df-clel 2811. (Revised by Gino Giotto, 6-Sep-2024.) |
Ref | Expression |
---|---|
eq0rdv.1 | ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) |
Ref | Expression |
---|---|
eq0rdv | ⊢ (𝜑 → 𝐴 = ∅) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eq0rdv.1 | . . 3 ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) | |
2 | 1 | alrimiv 1931 | . 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
3 | dfnul4 4325 | . . . 4 ⊢ ∅ = {𝑦 ∣ ⊥} | |
4 | 3 | eqeq2i 2746 | . . 3 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
5 | dfcleq 2726 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
6 | df-clab 2711 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
7 | sbv 2092 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
8 | 6, 7 | bitri 275 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
9 | 8 | bibi2i 338 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
10 | 9 | albii 1822 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥)) |
11 | nbfal 1557 | . . . . . 6 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
12 | 11 | bicomi 223 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) ↔ ¬ 𝑥 ∈ 𝐴) |
13 | 12 | albii 1822 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
14 | 10, 13 | bitri 275 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
15 | 4, 5, 14 | 3bitrri 298 | . 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅) |
16 | 2, 15 | sylib 217 | 1 ⊢ (𝜑 → 𝐴 = ∅) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∀wal 1540 = wceq 1542 ⊥wfal 1554 [wsb 2068 ∈ wcel 2107 {cab 2710 ∅c0 4323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-dif 3952 df-nul 4324 |
This theorem is referenced by: map0b 8877 disjen 9134 mapdom1 9142 pwxpndom2 10660 fzdisj 13528 smu01lem 16426 prmreclem5 16853 vdwap0 16909 natfval 17897 fucbas 17912 fuchom 17913 fuchomOLD 17914 coafval 18014 efgval 19585 lsppratlem6 20765 lbsextlem4 20774 psrvscafval 21509 cfinufil 23432 ufinffr 23433 fin1aufil 23436 bldisj 23904 reconnlem1 24342 pcofval 24526 bcthlem5 24845 volfiniun 25064 fta1g 25685 fta1 25821 rpvmasum 27029 0ringprmidl 32568 0ringmon1p 32636 0ringirng 32753 unblimceq0 35383 bj-ab0 35788 bj-projval 35877 finxpnom 36282 ipo0 43208 ifr0 43209 limclner 44367 |
Copyright terms: Public domain | W3C validator |