![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleq1w | GIF version |
Description: Weaker version of eleq1 2162 (but more general than elequ1 1658) not depending on ax-ext 2082 nor df-cleq 2093. (Contributed by BJ, 24-Jun-2019.) |
Ref | Expression |
---|---|
eleq1w | ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ2 1657 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦)) | |
2 | 1 | anbi1d 456 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ (𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))) |
3 | 2 | exbidv 1764 | . 2 ⊢ (𝑥 = 𝑦 → (∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴) ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴))) |
4 | df-clel 2096 | . 2 ⊢ (𝑥 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑧 ∈ 𝐴)) | |
5 | df-clel 2096 | . 2 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑧(𝑧 = 𝑦 ∧ 𝑧 ∈ 𝐴)) | |
6 | 3, 4, 5 | 3bitr4g 222 | 1 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∃wex 1436 ∈ wcel 1448 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 |
This theorem depends on definitions: df-bi 116 df-clel 2096 |
This theorem is referenced by: clelsb3f 2244 dfdif3 3133 dfss4st 3256 abn0m 3335 r19.2m 3396 cbvmptf 3962 iinexgm 4019 xpiindim 4614 cnviinm 5016 iinerm 6431 ixpiinm 6548 ixpsnf1o 6560 mapsnen 6635 enumctlemm 6913 exmidomni 6926 fodjum 6930 iseqf1olemqk 10108 seq3f1olemqsum 10114 summodclem2 10990 summodc 10991 zsumdc 10992 fsum3 10995 isumz 10997 isumss 10999 fisumss 11000 isumss2 11001 fsum3cvg2 11002 fsumsersdc 11003 fsum3ser 11005 fsumsplit 11015 fsumsplitf 11016 isumlessdc 11104 neipsm 12105 limcimo 12514 nninfalllemn 12786 |
Copyright terms: Public domain | W3C validator |