| 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 2110, df-clel 2816. (Revised by GG, 6-Sep-2024.) |
| Ref | Expression |
|---|---|
| eq0rdv.1 | ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) |
| Ref | Expression |
|---|---|
| eq0rdv | ⊢ (𝜑 → 𝐴 = ∅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eq0rdv.1 | . . 3 ⊢ (𝜑 → ¬ 𝑥 ∈ 𝐴) | |
| 2 | 1 | alrimiv 1927 | . 2 ⊢ (𝜑 → ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
| 3 | dfnul4 4335 | . . . 4 ⊢ ∅ = {𝑦 ∣ ⊥} | |
| 4 | 3 | eqeq2i 2750 | . . 3 ⊢ (𝐴 = ∅ ↔ 𝐴 = {𝑦 ∣ ⊥}) |
| 5 | dfcleq 2730 | . . 3 ⊢ (𝐴 = {𝑦 ∣ ⊥} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥})) | |
| 6 | df-clab 2715 | . . . . . . 7 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ [𝑥 / 𝑦]⊥) | |
| 7 | sbv 2088 | . . . . . . 7 ⊢ ([𝑥 / 𝑦]⊥ ↔ ⊥) | |
| 8 | 6, 7 | bitri 275 | . . . . . 6 ⊢ (𝑥 ∈ {𝑦 ∣ ⊥} ↔ ⊥) |
| 9 | 8 | bibi2i 337 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) |
| 10 | 9 | albii 1819 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥)) |
| 11 | nbfal 1555 | . . . . . 6 ⊢ (¬ 𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ↔ ⊥)) | |
| 12 | 11 | bicomi 224 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↔ ⊥) ↔ ¬ 𝑥 ∈ 𝐴) |
| 13 | 12 | albii 1819 | . . . 4 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ ⊥) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
| 14 | 10, 13 | bitri 275 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ {𝑦 ∣ ⊥}) ↔ ∀𝑥 ¬ 𝑥 ∈ 𝐴) |
| 15 | 4, 5, 14 | 3bitrri 298 | . 2 ⊢ (∀𝑥 ¬ 𝑥 ∈ 𝐴 ↔ 𝐴 = ∅) |
| 16 | 2, 15 | sylib 218 | 1 ⊢ (𝜑 → 𝐴 = ∅) |
| Colors of variables: wff setvar class |
| Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∀wal 1538 = wceq 1540 ⊥wfal 1552 [wsb 2064 ∈ wcel 2108 {cab 2714 ∅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-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-fal 1553 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-dif 3954 df-nul 4334 |
| This theorem is referenced by: map0b 8923 disjen 9174 mapdom1 9182 pwxpndom2 10705 fzdisj 13591 smu01lem 16522 prmreclem5 16958 vdwap0 17014 natfval 17994 fucbas 18008 fuchom 18009 coafval 18109 efgval 19735 lsppratlem6 21154 lbsextlem4 21163 psrvscafval 21968 cfinufil 23936 ufinffr 23937 fin1aufil 23940 bldisj 24408 reconnlem1 24848 pcofval 25043 bcthlem5 25362 volfiniun 25582 fta1g 26209 fta1 26350 rpvmasum 27570 0ringprmidl 33477 0ringmon1p 33583 0ringirng 33739 unblimceq0 36508 bj-ab0 36909 bj-projval 36997 finxpnom 37402 ipo0 44468 ifr0 44469 limclner 45666 |
| Copyright terms: Public domain | W3C validator |