![]() |
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 2175 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶) |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1312 ∈ wcel 1461 |
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 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-17 1487 ax-ial 1495 ax-ext 2095 |
This theorem depends on definitions: df-bi 116 df-cleq 2106 df-clel 2109 |
This theorem is referenced by: eleq12i 2180 eqeltri 2185 intexrabim 4036 abssexg 4064 abnex 4326 snnex 4327 pwexb 4353 sucexb 4371 omex 4465 iprc 4763 dfse2 4868 fressnfv 5559 fnotovb 5766 f1stres 6008 f2ndres 6009 ottposg 6103 dftpos4 6111 frecabex 6246 oacl 6307 diffifi 6738 djuexb 6878 pitonn 7576 axicn 7591 pnfnre 7724 mnfnre 7725 0mnnnnn0 8906 nprmi 11644 txdis1cn 12282 xmeterval 12417 expcncf 12571 bj-sucexg 12799 |
Copyright terms: Public domain | W3C validator |