Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleq1i | Unicode 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 2227 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wceq 1342 wcel 2135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-clel 2160 |
This theorem is referenced by: eleq12i 2232 eqeltri 2237 intexrabim 4126 abssexg 4155 abnex 4419 snnex 4420 pwexb 4446 sucexb 4468 omex 4564 iprc 4866 dfse2 4971 fressnfv 5666 fnotovb 5876 f1stres 6119 f2ndres 6120 ottposg 6214 dftpos4 6222 frecabex 6357 oacl 6419 diffifi 6851 djuexb 7000 pitonn 7780 axicn 7795 pnfnre 7931 mnfnre 7932 0mnnnnn0 9137 nprmi 12035 txdis1cn 12825 xmeterval 12982 expcncf 13139 bj-sucexg 13645 |
Copyright terms: Public domain | W3C validator |