Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eleq1a | Structured version Visualization version GIF 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 2900 | . 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
2 | 1 | biimprcd 251 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 ∈ wcel 2105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-clel 2893 |
This theorem is referenced by: elex2 3517 elex22 3518 clel5OLD 3657 disjne 4402 eqoreldif 4616 ordelinel 6283 ssimaex 6742 fnex 6972 f1ocnv2d 7387 peano5 7593 mpoexw 7767 tfrlem8 8011 tz7.48-2 8069 tz7.49 8072 eroprf 8385 onfin 8698 pssnn 8725 ac6sfi 8751 elfiun 8883 brwdom 9020 ficardom 9379 ficard 9976 tskxpss 10183 inar1 10186 rankcf 10188 tskuni 10194 gruun 10217 nsmallnq 10388 prnmadd 10408 genpss 10415 eqlei 10739 eqlei2 10740 renegcli 10936 supaddc 11597 supadd 11598 supmul1 11599 supmullem2 11601 supmul 11602 nn0ind-raph 12071 uzwo 12300 iccid 12773 hashvnfin 13711 hashdifsnp1 13844 mertenslem2 15231 4sqlem1 16274 4sqlem4 16278 4sqlem11 16281 symggen 18529 psgnran 18574 odlem1 18594 gexlem1 18635 gsumpr 19006 lssvneln0 19654 lss1d 19666 lspsn 19705 lsmelval2 19788 psgnghm 20654 opnneiid 21664 cmpsublem 21937 metrest 23063 metustel 23089 dscopn 23112 ovolshftlem2 24040 subopnmbl 24134 deg1ldgn 24616 plyremlem 24822 coseq0negpitopi 25018 ppiublem1 25706 mptelee 26609 nbuhgr2vtx1edgblem 27061 numclwwlk1lem2foa 28061 shsleji 29075 spansnss 29276 spansncvi 29357 f1o3d 30301 sigaclcu2 31279 measdivcstALTV 31384 dfon2lem6 32931 noextendseq 33072 bdayfo 33080 scutf 33171 altxpsspw 33336 hfun 33537 ontgval 33677 ordtoplem 33681 ordcmp 33693 findreccl 33699 bj-xpnzex 34169 bj-snsetex 34173 bj-ismooredr2 34297 bj-ideqg1 34349 topdifinfindis 34510 finxpreclem1 34553 ovoliunnfl 34816 volsupnfl 34819 heibor1lem 34970 heibor1 34971 lshpkrlem1 36128 lfl1dim 36139 leat3 36313 meetat2 36315 glbconxN 36396 pointpsubN 36769 pmapglbx 36787 linepsubclN 36969 dia2dimlem7 38088 dib1dim2 38186 diclspsn 38212 dih1dimatlem 38347 dihatexv2 38357 djhlsmcl 38432 fltne 39152 3cubes 39167 hbtlem2 39604 hbtlem5 39608 rp-isfinite6 39764 snssiALTVD 41041 snssiALT 41042 elex2VD 41052 elex22VD 41053 fveqvfvv 43156 afv0fv0 43229 lswn0 43451 lidlmmgm 44094 1neven 44101 cznrng 44124 |
Copyright terms: Public domain | W3C validator |