![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eqeltrdi | Unicode version |
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
eqeltrdi.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
eqeltrdi.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
eqeltrdi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltrdi.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqeltrdi.2 |
. . 3
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 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: eqeltrrdi 2232 snexprc 4118 onsucelsucexmidlem 4452 dcextest 4503 nnpredcl 4544 ovprc 5814 nnmcl 6385 xpsnen 6723 xpfi 6826 snexxph 6846 ctssdclemn0 7003 exmidonfinlem 7066 indpi 7174 nq0m0r 7288 genpelxp 7343 un0mulcl 9035 znegcl 9109 zeo 9180 eqreznegel 9433 xnegcl 9645 modqid0 10154 q2txmodxeq0 10188 ser0 10318 expcllem 10335 m1expcl2 10346 bcval 10527 bccl 10545 hashinfom 10556 resqrexlemlo 10817 iserge0 11144 sumrbdclem 11178 fsum3cvg 11179 summodclem3 11181 summodclem2a 11182 fisumss 11193 binom 11285 bcxmas 11290 prodf1 11343 prodrbdclem 11372 fproddccvg 11373 prodmodclem2a 11377 gcdval 11684 gcdcl 11691 lcmcl 11789 ssblps 12633 ssbl 12634 xmeter 12644 blssioo 12753 012of 13363 2o01f 13364 nninfsellemeqinf 13387 nninffeq 13391 trilpolemclim 13404 |
Copyright terms: Public domain | W3C validator |