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 2827 | . 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
2 | 1 | biimprcd 249 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1539 ∈ wcel 2107 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2710 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1783 df-cleq 2731 df-clel 2817 |
This theorem is referenced by: elex2OLD 3454 elex22 3455 disj 4382 disjne 4389 elpr2g 4586 eqoreldif 4621 ordelinel 6368 onun2 6374 ssimaex 6862 fnex 7102 f1ocnv2d 7531 peano5 7749 peano5OLD 7750 mpoexw 7928 tfrlem8 8224 tz7.48-2 8282 tz7.49 8285 eroprf 8613 pssnn 8960 onfin 9022 pssnnOLD 9049 ac6sfi 9067 elfiun 9198 brwdom 9335 ficardom 9728 ficard 10330 tskxpss 10537 inar1 10540 rankcf 10542 tskuni 10548 gruun 10571 nsmallnq 10742 prnmadd 10762 genpss 10769 eqlei 11094 eqlei2 11095 renegcli 11291 supaddc 11951 supadd 11952 supmul1 11953 supmullem2 11955 supmul 11956 nn0ind-raph 12429 uzwo 12660 iccid 13133 hashvnfin 14084 hashdifsnp1 14219 mertenslem2 15606 4sqlem1 16658 4sqlem4 16662 4sqlem11 16665 symggen 19087 psgnran 19132 odlem1 19152 gexlem1 19193 gsumpr 19565 lssvneln0 20222 lss1d 20234 lspsn 20273 lsmelval2 20356 psgnghm 20794 opnneiid 22286 cmpsublem 22559 metrest 23689 metustel 23715 dscopn 23738 ovolshftlem2 24683 subopnmbl 24777 deg1ldgn 25267 plyremlem 25473 coseq0negpitopi 25669 ppiublem1 26359 mptelee 27272 nbuhgr2vtx1edgblem 27727 numclwwlk1lem2foa 28727 shsleji 29741 spansnss 29942 spansncvi 30023 f1o3d 30971 sigaclcu2 32097 measdivcstALTV 32202 dfon2lem6 33773 noextendseq 33879 bdayfo 33889 scutf 34015 altxpsspw 34288 hfun 34489 ontgval 34629 ordtoplem 34633 ordcmp 34645 findreccl 34651 bj-xpnzex 35158 bj-snsetex 35162 bj-ismooredr2 35290 bj-ideqg1 35344 topdifinfindis 35526 finxpreclem1 35569 ovoliunnfl 35828 volsupnfl 35831 heibor1lem 35976 heibor1 35977 lshpkrlem1 37131 lfl1dim 37142 leat3 37316 meetat2 37318 glbconxN 37399 pointpsubN 37772 pmapglbx 37790 linepsubclN 37972 dia2dimlem7 39091 dib1dim2 39189 diclspsn 39215 dih1dimatlem 39350 dihatexv2 39360 djhlsmcl 39435 fsuppssind 40289 fltne 40488 3cubes 40519 hbtlem2 40956 hbtlem5 40960 rp-isfinite6 41132 snssiALTVD 42454 snssiALT 42455 elex2VD 42465 elex22VD 42466 fveqvfvv 44545 afv0fv0 44652 lswn0 44907 lidlmmgm 45494 1neven 45501 cznrng 45524 upwordnul 46526 upwordsing 46530 tworepnotupword 46532 |
Copyright terms: Public domain | W3C validator |