![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eleq1i | GIF version |
Description: Inference from equality to equivalence of membership. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
eleq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
eleq1i | ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | eleq1 2252 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 105 = wceq 1364 ∈ wcel 2160 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-ial 1545 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-cleq 2182 df-clel 2185 |
This theorem is referenced by: eleq12i 2257 eqeltri 2262 intexrabim 4171 abssexg 4200 abnex 4465 snnex 4466 pwexb 4492 sucexb 4514 omex 4610 iprc 4913 dfse2 5019 fressnfv 5724 fnotovb 5939 f1stres 6184 f2ndres 6185 ottposg 6280 dftpos4 6288 frecabex 6423 oacl 6485 diffifi 6922 djuexb 7073 pitonn 7877 axicn 7892 pnfnre 8029 mnfnre 8030 0mnnnnn0 9238 nprmi 12156 issubm 12924 issrg 13319 srgfcl 13327 subrngrng 13549 txdis1cn 14238 xmeterval 14395 expcncf 14552 bj-sucexg 15135 |
Copyright terms: Public domain | W3C validator |