![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeltrid | Unicode version |
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
eqeltrid.1 |
![]() ![]() ![]() ![]() |
eqeltrid.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqeltrid |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltrid.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | eqeltrid.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | eqeltrd 2217 |
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 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-4 1488 ax-17 1507 ax-ial 1515 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-cleq 2133 df-clel 2136 |
This theorem is referenced by: eqeltrrid 2228 csbexga 4064 otexg 4160 tpexg 4373 dmresexg 4850 f1oabexg 5387 funfvex 5446 riotaexg 5742 riotaprop 5761 fnovex 5812 ovexg 5813 fovrn 5921 fnovrn 5926 cofunexg 6017 cofunex2g 6018 abrexex2g 6026 xpexgALT 6039 mpofvex 6109 tfrex 6273 frec0g 6302 freccllem 6307 ecexg 6441 qsexg 6493 pmex 6555 elixpsn 6637 diffifi 6796 unfidisj 6818 prfidisj 6823 tpfidisj 6824 ssfirab 6830 ssfidc 6831 fnfi 6833 funrnfi 6838 iunfidisj 6842 infclti 6918 djuex 6936 ctssdccl 7004 addvalex 7676 negcl 7986 intqfrac2 10123 intfracq 10124 frec2uzzd 10204 frecuzrdgrrn 10212 iseqf1olemqpcl 10300 seq3f1olemqsum 10304 bcval5 10541 xrmaxiflemval 11051 climmpt 11101 reccn2ap 11114 zsumdc 11185 fsumzcl2 11206 fsump1i 11234 fsumabs 11266 hash2iun1dif1 11281 mertenslemi1 11336 algrf 11762 algcvg 11765 algcvga 11768 algfx 11769 eucalgcvga 11775 eucalg 11776 crth 11936 phimullem 11937 ennnfonelemj0 11950 ennnfonelemom 11957 ressid 12059 1strbas 12097 2strbasg 12099 2stropg 12100 restid 12170 topnvalg 12171 topnidg 12172 topopn 12214 topcld 12317 uncld 12321 iuncld 12323 unicld 12324 tgrest 12377 restin 12384 cnco 12429 cnrest 12443 cnptoprest2 12448 lmss 12454 txbasval 12475 txcn 12483 cnmpt12f 12494 hmeoco 12524 idhmeo 12525 blres 12642 metrest 12714 qtopbasss 12729 tgqioo 12755 divcnap 12763 fsumcncntop 12764 cncfmet 12787 cdivcncfap 12795 cnrehmeocntop 12801 cnplimcim 12844 limccnpcntop 12852 limccnp2lem 12853 limccnp2cntop 12854 dvfvalap 12858 bj-snexg 13281 trilpolemcl 13405 |
Copyright terms: Public domain | W3C validator |