![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE 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 10 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | syl5eqel.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqeltrd 2427 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-an 360 df-ex 1542 df-cleq 2346 df-clel 2349 |
This theorem is referenced by: syl5eqelr 2438 csbexg 3146 complexg 4099 inexg 4100 unexg 4101 difexg 4102 symdifexg 4103 uni1exg 4292 imakexg 4299 pw1exg 4302 cokexg 4309 imagekexg 4311 uniexg 4316 intexg 4319 pwexg 4328 addcexg 4393 nncaddccl 4419 ltfintr 4459 ncfinprop 4474 tfinprop 4489 nnadjoinpw 4521 sfindbl 4530 phiexg 4571 opexg 4587 proj1exg 4591 proj2exg 4592 imaexg 4746 coexg 4749 siexg 4752 cnvexg 5101 rnexg 5104 dmexg 5105 xpexg 5114 resexg 5116 fovrn 5604 fnovrn 5607 txpexg 5784 fixexg 5788 ins2exg 5795 ins3exg 5796 imageexg 5800 pprodexg 5837 fullfunexg 5859 ecexg 5949 qsexg 5982 pmex 6005 pmvalg 6010 nenpw1pwlem1 6084 tccl 6160 frecexg 6312 |
Copyright terms: Public domain | W3C validator |