Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eleq1a | Structured version Visualization version Unicode version |
Description: A transitive-type law relating membership and equality. (Contributed by NM, 9-Apr-1994.) |
Ref | Expression |
---|---|
eleq1a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2689 | . 2 | |
2 | 1 | biimprcd 240 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wceq 1483 wcel 1990 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-clel 2618 |
This theorem is referenced by: elex2 3216 elex22 3217 clel5 3343 reu6 3395 disjne 4022 eqoreldif 4225 ordelinel 5825 ssimaex 6263 fnex 6481 f1ocnv2d 6886 peano5 7089 tfrlem8 7480 tz7.48-2 7537 tz7.49 7540 eroprf 7845 onfin 8151 pssnn 8178 ac6sfi 8204 elfiun 8336 brwdom 8472 ficardom 8787 ficard 9387 tskxpss 9594 inar1 9597 rankcf 9599 tskuni 9605 gruun 9628 nsmallnq 9799 prnmadd 9819 genpss 9826 eqlei 10147 eqlei2 10148 renegcli 10342 supaddc 10990 supadd 10991 supmul1 10992 supmullem2 10994 supmul 10995 nn0ind-raph 11477 uzwo 11751 iccid 12220 hashvnfin 13151 brfi1indlem 13278 mertenslem2 14617 4sqlem1 15652 4sqlem4 15656 4sqlem11 15659 symggen 17890 psgnran 17935 odlem1 17954 gexlem1 17994 lssneln0 18952 lss1d 18963 lspsn 19002 lsmelval2 19085 psgnghm 19926 opnneiid 20930 cmpsublem 21202 metrest 22329 metustel 22355 dscopn 22378 ovolshftlem2 23278 subopnmbl 23372 deg1ldgn 23853 plyremlem 24059 coseq0negpitopi 24255 ppiublem1 24927 mptelee 25775 nbuhgr2vtx1edgblem 26247 numclwlk1lem2foa 27224 shsleji 28229 spansnss 28430 spansncvi 28511 f1o3d 29431 sigaclcu2 30183 measdivcstOLD 30287 dfon2lem6 31693 noextendseq 31820 bdayfo 31828 scutf 31919 altxpsspw 32084 hfun 32285 ontgval 32430 ordtoplem 32434 ordcmp 32446 findreccl 32452 bj-xpnzex 32946 bj-snsetex 32951 topdifinfindis 33194 finxpreclem1 33226 ovoliunnfl 33451 volsupnfl 33454 heibor1lem 33608 heibor1 33609 lshpkrlem1 34397 lfl1dim 34408 leat3 34582 meetat2 34584 glbconxN 34664 pointpsubN 35037 pmapglbx 35055 linepsubclN 35237 dia2dimlem7 36359 dib1dim2 36457 diclspsn 36483 dih1dimatlem 36618 dihatexv2 36628 djhlsmcl 36703 hbtlem2 37694 hbtlem5 37698 rp-isfinite6 37864 snssiALTVD 39062 snssiALT 39063 elex2VD 39073 elex22VD 39074 fveqvfvv 41204 afv0fv0 41229 lswn0 41380 lidlmmgm 41925 1neven 41932 cznrng 41955 gsumpr 42139 |
Copyright terms: Public domain | W3C validator |