![]() |
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 2718 | . 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
2 | 1 | biimprcd 240 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ∈ wcel 2030 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 df-clel 2647 |
This theorem is referenced by: elex2 3247 elex22 3248 clel5 3375 reu6 3428 disjne 4055 eqoreldif 4257 ordelinel 5863 ssimaex 6302 fnex 6522 f1ocnv2d 6928 peano5 7131 tfrlem8 7525 tz7.48-2 7582 tz7.49 7585 eroprf 7888 onfin 8192 pssnn 8219 ac6sfi 8245 elfiun 8377 brwdom 8513 ficardom 8825 ficard 9425 tskxpss 9632 inar1 9635 rankcf 9637 tskuni 9643 gruun 9666 nsmallnq 9837 prnmadd 9857 genpss 9864 eqlei 10185 eqlei2 10186 renegcli 10380 supaddc 11028 supadd 11029 supmul1 11030 supmullem2 11032 supmul 11033 nn0ind-raph 11515 uzwo 11789 iccid 12258 hashvnfin 13189 brfi1indlem 13316 mertenslem2 14661 4sqlem1 15699 4sqlem4 15703 4sqlem11 15706 symggen 17936 psgnran 17981 odlem1 18000 gexlem1 18040 lssneln0 19000 lss1d 19011 lspsn 19050 lsmelval2 19133 psgnghm 19974 opnneiid 20978 cmpsublem 21250 metrest 22376 metustel 22402 dscopn 22425 ovolshftlem2 23324 subopnmbl 23418 deg1ldgn 23898 plyremlem 24104 coseq0negpitopi 24300 ppiublem1 24972 mptelee 25820 nbuhgr2vtx1edgblem 26292 clwwlknonwwlknonbOLD 27081 numclwlk1lem2foa 27344 shsleji 28357 spansnss 28558 spansncvi 28639 f1o3d 29559 sigaclcu2 30311 measdivcstOLD 30415 dfon2lem6 31817 noextendseq 31945 bdayfo 31953 scutf 32044 altxpsspw 32209 hfun 32410 ontgval 32555 ordtoplem 32559 ordcmp 32571 findreccl 32577 bj-xpnzex 33071 bj-snsetex 33076 topdifinfindis 33324 finxpreclem1 33356 ovoliunnfl 33581 volsupnfl 33584 heibor1lem 33738 heibor1 33739 lshpkrlem1 34715 lfl1dim 34726 leat3 34900 meetat2 34902 glbconxN 34982 pointpsubN 35355 pmapglbx 35373 linepsubclN 35555 dia2dimlem7 36676 dib1dim2 36774 diclspsn 36800 dih1dimatlem 36935 dihatexv2 36945 djhlsmcl 37020 hbtlem2 38011 hbtlem5 38015 rp-isfinite6 38181 snssiALTVD 39376 snssiALT 39377 elex2VD 39387 elex22VD 39388 fveqvfvv 41525 afv0fv0 41550 lswn0 41705 lidlmmgm 42250 1neven 42257 cznrng 42280 gsumpr 42464 |
Copyright terms: Public domain | W3C validator |