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 2216 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 wcel 1480 |
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 1423 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-4 1487 ax-17 1506 ax-ial 1514 ax-ext 2121 |
This theorem depends on definitions: df-bi 116 df-cleq 2132 df-clel 2135 |
This theorem is referenced by: eqeltrrdi 2231 snexprc 4110 onsucelsucexmidlem 4444 dcextest 4495 nnpredcl 4536 ovprc 5806 nnmcl 6377 xpsnen 6715 xpfi 6818 snexxph 6838 ctssdclemn0 6995 exmidonfinlem 7049 indpi 7153 nq0m0r 7267 genpelxp 7322 un0mulcl 9014 znegcl 9088 zeo 9159 eqreznegel 9409 xnegcl 9618 modqid0 10126 q2txmodxeq0 10160 ser0 10290 expcllem 10307 m1expcl2 10318 bcval 10498 bccl 10516 hashinfom 10527 resqrexlemlo 10788 iserge0 11115 sumrbdclem 11149 fsum3cvg 11150 summodclem3 11152 summodclem2a 11153 fisumss 11164 binom 11256 bcxmas 11261 prodf1 11314 prodrbdclem 11343 fproddccvg 11344 prodmodclem2a 11348 gcdval 11651 gcdcl 11658 lcmcl 11756 ssblps 12597 ssbl 12598 xmeter 12608 blssioo 12717 nninfsellemeqinf 13215 nninffeq 13219 isomninnlem 13228 trilpolemclim 13232 |
Copyright terms: Public domain | W3C validator |