Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eqeltrri | Structured version Visualization version GIF version |
Description: Substitution of equal classes into membership relation. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
eqeltrri.1 | ⊢ 𝐴 = 𝐵 |
eqeltrri.2 | ⊢ 𝐴 ∈ 𝐶 |
Ref | Expression |
---|---|
eqeltrri | ⊢ 𝐵 ∈ 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeltrri.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 1 | eqcomi 2830 | . 2 ⊢ 𝐵 = 𝐴 |
3 | eqeltrri.2 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
4 | 2, 3 | eqeltri 2909 | 1 ⊢ 𝐵 ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = 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: 3eltr3i 2925 zfrep4 5192 p0ex 5276 pp0ex 5278 ord3ex 5279 zfpair 5313 epse 5532 unex 7457 fvresex 7652 opabex3 7659 abexssex 7662 abexex 7663 oprabrexex2 7670 seqomlem3 8079 inf0 9073 scottexs 9305 kardex 9312 infxpenlem 9428 r1om 9655 cfon 9666 fin23lem16 9746 fin1a2lem6 9816 hsmexlem5 9841 brdom7disj 9942 brdom6disj 9943 1lt2pi 10316 0cn 10622 resubcli 10937 0reALT 10972 1nn 11638 10nn 12103 numsucc 12127 nummac 12132 unirnioo 12827 ioorebas 12829 fz0to4untppr 13000 om2uzrani 13310 uzrdg0i 13317 hashunlei 13776 cats1fvn 14210 trclubi 14346 4sqlem19 16289 dec2dvds 16389 mod2xnegi 16397 modsubi 16398 gcdi 16399 isstruct2 16483 grppropstr 18060 ltbval 20182 nn0srg 20545 sn0topon 21536 indistop 21540 indisuni 21541 indistps2 21550 indistps2ALT 21552 restbas 21696 leordtval2 21750 iocpnfordt 21753 icomnfordt 21754 iooordt 21755 reordt 21756 dis1stc 22037 ptcmpfi 22351 ustfn 22739 ustn0 22758 retopbas 23298 blssioo 23332 xrtgioo 23343 zcld 23350 cnperf 23357 retopconn 23366 iimulcn 23471 rembl 24070 mbfdm 24156 ismbf 24158 mbf0 24164 abelthlem9 24957 advlog 25164 advlogexp 25165 2irrexpq 25240 cxpcn3 25256 loglesqrt 25266 log2ub 25455 ppi1i 25673 cht2 25677 cht3 25678 bpos1lem 25786 lgslem4 25804 vmadivsum 25986 log2sumbnd 26048 selberg2 26055 selbergr 26072 iscgrg 26226 ishpg 26473 ax5seglem7 26649 h2hva 28679 h2hsm 28680 h2hnm 28681 norm-ii-i 28842 hhshsslem2 28973 shincli 29067 chincli 29165 lnophdi 29707 imaelshi 29763 rnelshi 29764 bdophdi 29802 dfdec100 30474 dpadd2 30514 dpmul 30517 dpmul4 30518 nn0omnd 30842 nn0archi 30844 ccfldextrr 30938 lmatfvlem 30980 rmulccn 31071 rrhre 31162 sigaex 31269 br2base 31427 sxbrsigalem3 31430 carsgclctunlem3 31478 sitmcl 31509 rpsqrtcn 31764 hgt750lem 31822 hgt750lem2 31823 afsval 31842 kur14lem7 32357 retopsconn 32394 satfvsuclem1 32504 fmlasuc0 32529 hfuni 33543 neibastop2lem 33606 onint1 33695 topdifinffinlem 34511 poimirlem9 34783 poimirlem28 34802 poimirlem30 34804 poimirlem32 34806 bddiblnc 34844 ftc1cnnc 34848 cncfres 34926 lineset 36756 lautset 37100 pautsetN 37116 tendoset 37777 decpmulnc 39053 decpmul 39054 areaquad 39703 sblpnf 40522 lhe4.4ex1a 40541 fourierdlem62 42334 fourierdlem76 42348 65537prm 43585 11gbo 43787 bgoldbtbndlem1 43817 |
Copyright terms: Public domain | W3C validator |