![]() |
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 2097 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 7 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1333 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-4 1397 ax-17 1416 ax-ial 1424 ax-ext 2019 |
This theorem depends on definitions: df-bi 110 df-cleq 2030 df-clel 2033 |
This theorem is referenced by: eleq12i 2102 eqeltri 2107 intexrabim 3898 abssexg 3925 snnex 4147 pwexb 4172 sucexb 4189 omex 4259 iprc 4543 dfse2 4641 fressnfv 5293 fnotovb 5490 f1stres 5728 f2ndres 5729 ottposg 5811 dftpos4 5819 frecabex 5923 oacl 5979 pitonn 6744 axicn 6749 pnfnre 6864 mnfnre 6865 0mnnnnn0 7990 bj-sucexg 9377 |
Copyright terms: Public domain | W3C validator |