Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > syl6eqel | Unicode version |
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
syl6eqel.1 | |
syl6eqel.2 |
Ref | Expression |
---|---|
syl6eqel |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6eqel.1 | . 2 | |
2 | syl6eqel.2 | . . 3 | |
3 | 2 | a1i 9 | . 2 |
4 | 1, 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: syl6eqelr 2129 snexprc 3938 onsucelsucexmidlem 4254 ovprc 5540 nnmcl 6060 xpsnen 6295 indpi 6440 nq0m0r 6554 genpelxp 6609 un0mulcl 8216 znegcl 8276 zeo 8343 eqreznegel 8549 xnegcl 8745 iser0 9250 expival 9257 expcllem 9266 m1expcl2 9277 resqrexlemlo 9611 iserige0 9863 |
Copyright terms: Public domain | W3C validator |