Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eleq1w | Unicode version |
Description: Weaker version of eleq1 2180 (but more general than elequ1 1675) not depending on ax-ext 2099 nor df-cleq 2110. (Contributed by BJ, 24-Jun-2019.) |
Ref | Expression |
---|---|
eleq1w |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ2 1674 | . . . 4 | |
2 | 1 | anbi1d 460 | . . 3 |
3 | 2 | exbidv 1781 | . 2 |
4 | df-clel 2113 | . 2 | |
5 | df-clel 2113 | . 2 | |
6 | 3, 4, 5 | 3bitr4g 222 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wb 104 wex 1453 wcel 1465 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-clel 2113 |
This theorem is referenced by: clelsb3f 2262 dfdif3 3156 dfss4st 3279 abn0m 3358 r19.2m 3419 cbvmptf 3992 iinexgm 4049 xpiindim 4646 cnviinm 5050 iinerm 6469 ixpiinm 6586 ixpsnf1o 6598 mapsnen 6673 enumctlemm 6967 exmidomni 6982 fodjum 6986 suplocexprlemmu 7494 suplocsr 7585 axpre-suploc 7678 iseqf1olemqk 10222 seq3f1olemqsum 10228 summodclem2 11106 summodc 11107 zsumdc 11108 fsum3 11111 isumz 11113 isumss 11115 fisumss 11116 isumss2 11117 fsum3cvg2 11118 fsumsersdc 11119 fsum3ser 11121 fsumsplit 11131 fsumsplitf 11132 isumlessdc 11220 neipsm 12234 dedekindeulemub 12676 dedekindeulemloc 12677 dedekindeulemlub 12678 suplociccex 12683 dedekindicclemub 12685 dedekindicclemloc 12686 dedekindicclemlub 12687 limcimo 12714 nninfalllemn 13098 |
Copyright terms: Public domain | W3C validator |