| 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 2829 | . 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
| 2 | 1 | biimprcd 250 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-clel 2816 |
| This theorem is referenced by: elex2OLD 3505 elex22 3506 disj 4450 disjne 4455 rabsneq 4644 elpr2g 4651 eqoreldif 4685 ordelinel 6485 onun2 6492 ssimaex 6994 fnex 7237 f1ocnv2d 7686 omun 7909 peano5 7915 mpoexw 8103 tfrlem8 8424 tz7.48-2 8482 tz7.49 8485 eroprf 8855 pssnn 9208 onfin 9267 ac6sfi 9320 elfiun 9470 brwdom 9607 ficardom 10001 ficard 10605 tskxpss 10812 inar1 10815 rankcf 10817 tskuni 10823 gruun 10846 nsmallnq 11017 prnmadd 11037 genpss 11044 mpoaddf 11249 mpomulf 11250 eqlei 11371 eqlei2 11372 renegcli 11570 supaddc 12235 supadd 12236 supmul1 12237 supmullem2 12239 supmul 12240 nn0ind-raph 12718 uzwo 12953 iccid 13432 hashvnfin 14399 hashdifsnp1 14545 mertenslem2 15921 4sqlem1 16986 4sqlem4 16990 4sqlem11 16993 symggen 19488 psgnran 19533 odlem1 19553 gexlem1 19597 gsumpr 19973 lssvneln0 20950 lss1d 20961 lspsn 21000 lsmelval2 21084 rnglidlmmgm 21255 psgnghm 21598 opnneiid 23134 cmpsublem 23407 metrest 24537 metustel 24563 dscopn 24586 ovolshftlem2 25545 subopnmbl 25639 deg1ldgn 26132 plyremlem 26346 coseq0negpitopi 26545 ppiublem1 27246 noextendseq 27712 bdayfo 27722 scutf 27857 addsproplem2 28003 mptelee 28910 nbuhgr2vtx1edgblem 29368 numclwwlk1lem2foa 30373 shsleji 31389 spansnss 31590 spansncvi 31671 f1o3d 32637 sigaclcu2 34121 measdivcstALTV 34226 dfon2lem6 35789 altxpsspw 35978 hfun 36179 ontgval 36432 ordtoplem 36436 ordcmp 36448 findreccl 36454 bj-xpnzex 36960 bj-snsetex 36964 bj-ismooredr2 37111 bj-ideqg1 37165 topdifinfindis 37347 finxpreclem1 37390 ovoliunnfl 37669 volsupnfl 37672 heibor1lem 37816 heibor1 37817 lshpkrlem1 39111 lfl1dim 39122 leat3 39296 meetat2 39298 glbconxN 39380 pointpsubN 39753 pmapglbx 39771 linepsubclN 39953 dia2dimlem7 41072 dib1dim2 41170 diclspsn 41196 dih1dimatlem 41331 dihatexv2 41341 djhlsmcl 41416 fsuppssind 42603 fltne 42654 3cubes 42701 hbtlem2 43136 hbtlem5 43140 rp-isfinite6 43531 snssiALTVD 44847 snssiALT 44848 elex2VD 44858 elex22VD 44859 upwordnul 46895 upwordsing 46899 tworepnotupword 46901 fveqvfvv 47052 afv0fv0 47161 lswn0 47431 1neven 48154 cznrng 48177 |
| Copyright terms: Public domain | W3C validator |