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 2820 | . 2 ⊢ (𝐶 = 𝐴 → (𝐶 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵)) | |
2 | 1 | biimprcd 253 | 1 ⊢ (𝐴 ∈ 𝐵 → (𝐶 = 𝐴 → 𝐶 ∈ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 ∈ wcel 2114 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1787 df-cleq 2730 df-clel 2811 |
This theorem is referenced by: elex2 3419 elex22 3420 disj 4337 disjne 4344 elpr2g 4540 eqoreldif 4575 ordelinel 6270 onun2 6276 ssimaex 6753 fnex 6990 f1ocnv2d 7414 peano5 7624 peano5OLD 7625 mpoexw 7802 tfrlem8 8049 tz7.48-2 8107 tz7.49 8110 eroprf 8426 pssnn 8767 onfin 8789 pssnnOLD 8815 ac6sfi 8836 elfiun 8967 brwdom 9104 ficardom 9463 ficard 10065 tskxpss 10272 inar1 10275 rankcf 10277 tskuni 10283 gruun 10306 nsmallnq 10477 prnmadd 10497 genpss 10504 eqlei 10828 eqlei2 10829 renegcli 11025 supaddc 11685 supadd 11686 supmul1 11687 supmullem2 11689 supmul 11690 nn0ind-raph 12163 uzwo 12393 iccid 12866 hashvnfin 13813 hashdifsnp1 13948 mertenslem2 15333 4sqlem1 16384 4sqlem4 16388 4sqlem11 16391 symggen 18716 psgnran 18761 odlem1 18781 gexlem1 18822 gsumpr 19194 lssvneln0 19842 lss1d 19854 lspsn 19893 lsmelval2 19976 psgnghm 20396 opnneiid 21877 cmpsublem 22150 metrest 23277 metustel 23303 dscopn 23326 ovolshftlem2 24262 subopnmbl 24356 deg1ldgn 24846 plyremlem 25052 coseq0negpitopi 25248 ppiublem1 25938 mptelee 26841 nbuhgr2vtx1edgblem 27293 numclwwlk1lem2foa 28291 shsleji 29305 spansnss 29506 spansncvi 29587 f1o3d 30536 sigaclcu2 31658 measdivcstALTV 31763 dfon2lem6 33338 noextendseq 33513 bdayfo 33523 scutf 33649 altxpsspw 33922 hfun 34123 ontgval 34263 ordtoplem 34267 ordcmp 34279 findreccl 34285 bj-xpnzex 34792 bj-snsetex 34796 bj-ismooredr2 34922 bj-ideqg1 34976 topdifinfindis 35160 finxpreclem1 35203 ovoliunnfl 35462 volsupnfl 35465 heibor1lem 35610 heibor1 35611 lshpkrlem1 36767 lfl1dim 36778 leat3 36952 meetat2 36954 glbconxN 37035 pointpsubN 37408 pmapglbx 37426 linepsubclN 37608 dia2dimlem7 38727 dib1dim2 38825 diclspsn 38851 dih1dimatlem 38986 dihatexv2 38996 djhlsmcl 39071 fsuppssind 39881 fltne 40073 3cubes 40104 hbtlem2 40541 hbtlem5 40545 rp-isfinite6 40699 snssiALTVD 42005 snssiALT 42006 elex2VD 42016 elex22VD 42017 fveqvfvv 44093 afv0fv0 44194 lswn0 44450 lidlmmgm 45037 1neven 45044 cznrng 45067 |
Copyright terms: Public domain | W3C validator |