![]() |
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 4285 | . . . 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 4283 |
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 3914 df-nul 4284 |
This theorem is referenced by: map0b 8824 disjen 9081 mapdom1 9089 pwxpndom2 10606 fzdisj 13474 smu01lem 16370 prmreclem5 16797 vdwap0 16853 natfval 17838 fucbas 17853 fuchom 17854 fuchomOLD 17855 coafval 17955 efgval 19504 lsppratlem6 20629 lbsextlem4 20638 psrvscafval 21374 cfinufil 23295 ufinffr 23296 fin1aufil 23299 bldisj 23767 reconnlem1 24205 pcofval 24389 bcthlem5 24708 volfiniun 24927 fta1g 25548 fta1 25684 rpvmasum 26890 0ringprmidl 32270 0ringmon1p 32312 0ringirng 32420 unblimceq0 35016 bj-ab0 35421 bj-projval 35513 finxpnom 35918 ipo0 42817 ifr0 42818 limclner 43978 |
Copyright terms: Public domain | W3C validator |