![]() |
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 2252 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
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 4168 abssexg 4197 abnex 4462 snnex 4463 pwexb 4489 sucexb 4511 omex 4607 iprc 4910 dfse2 5016 fressnfv 5719 fnotovb 5934 f1stres 6178 f2ndres 6179 ottposg 6274 dftpos4 6282 frecabex 6417 oacl 6479 diffifi 6912 djuexb 7061 pitonn 7865 axicn 7880 pnfnre 8017 mnfnre 8018 0mnnnnn0 9226 nprmi 12142 issubm 12890 issrg 13280 srgfcl 13288 subrngrng 13510 txdis1cn 14175 xmeterval 14332 expcncf 14489 bj-sucexg 15071 |
Copyright terms: Public domain | W3C validator |