Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl5eqel | Unicode version |
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
syl5eqel.1 | |
syl5eqel.2 |
Ref | Expression |
---|---|
syl5eqel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5eqel.1 | . . 3 | |
2 | 1 | a1i 9 | . 2 |
3 | syl5eqel.2 | . 2 | |
4 | 2, 3 | eqeltrd 2114 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1243 wcel 1393 |
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 1336 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-4 1400 ax-17 1419 ax-ial 1427 ax-ext 2022 |
This theorem depends on definitions: df-bi 110 df-cleq 2033 df-clel 2036 |
This theorem is referenced by: syl5eqelr 2125 csbexga 3885 otexg 3967 tpexg 4179 dmresexg 4634 f1oabexg 5138 funfvex 5192 riotaexg 5472 riotaprop 5491 fnovex 5538 ovexg 5539 fovrn 5643 fnovrn 5648 cofunexg 5738 cofunex2g 5739 abrexex2g 5747 xpexgALT 5760 mpt2fvex 5829 tfrex 5954 frec0g 5983 ecexg 6110 qsexg 6162 diffifi 6351 addvalex 6920 negcl 7211 intqfrac2 9161 intfracq 9162 frecuzrdgrrn 9194 climmpt 9821 ialgcvg 9887 ialgcvga 9890 ialgfx 9891 bj-snexg 10032 |
Copyright terms: Public domain | W3C validator |