![]() |
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 2745 | . 2 ⊢ 𝐵 = 𝐴 |
3 | eqeltrri.2 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
4 | 2, 3 | eqeltri 2834 | 1 ⊢ 𝐵 ∈ 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2728 df-clel 2814 |
This theorem is referenced by: 3eltr3i 2850 zfrep4 5253 p0ex 5339 pp0ex 5341 ord3ex 5342 zfpair 5376 epse 5616 unex 7679 fvresex 7891 opabex3 7899 abexssex 7902 abexex 7903 oprabrexex2 7910 seqomlem3 8397 1on 8423 2on 8425 inf0 9556 scottexs 9822 kardex 9829 infxpenlem 9948 r1om 10179 cfon 10190 fin23lem16 10270 fin1a2lem6 10340 hsmexlem5 10365 brdom7disj 10466 brdom6disj 10467 1lt2pi 10840 0cn 11146 resubcli 11462 0reALT 11497 1nn 12163 10nn 12633 numsucc 12657 nummac 12662 unirnioo 13365 ioorebas 13367 fz0to4untppr 13543 om2uzrani 13856 uzrdg0i 13863 hashunlei 14324 cats1fvn 14746 trclubi 14880 4sqlem19 16834 dec2dvds 16934 mod2xnegi 16942 modsubi 16943 gcdi 16944 isstruct2 17020 grppropstr 18766 nn0srg 20865 ltbval 21442 sn0topon 22346 indistop 22350 indisuni 22351 indistps2 22360 indistps2ALT 22363 restbas 22507 leordtval2 22561 iocpnfordt 22564 icomnfordt 22565 iooordt 22566 reordt 22567 dis1stc 22848 ptcmpfi 23162 ustfn 23551 ustn0 23570 retopbas 24122 blssioo 24156 xrtgioo 24167 zcld 24174 cnperf 24181 retopconn 24190 iimulcn 24299 rembl 24902 mbfdm 24988 ismbf 24990 mbf0 24996 bddiblnc 25204 abelthlem9 25797 advlog 26007 advlogexp 26008 2irrexpq 26083 cxpcn3 26099 loglesqrt 26109 log2ub 26297 ppi1i 26515 cht2 26519 cht3 26520 bpos1lem 26628 lgslem4 26646 vmadivsum 26828 log2sumbnd 26890 selberg2 26897 selbergr 26914 nogt01o 27042 iscgrg 27452 ishpg 27699 ax5seglem7 27882 h2hva 29914 h2hsm 29915 h2hnm 29916 norm-ii-i 30077 hhshsslem2 30208 shincli 30302 chincli 30400 lnophdi 30942 imaelshi 30998 rnelshi 30999 bdophdi 31037 dfdec100 31721 dpadd2 31761 dpmul 31764 dpmul4 31765 nn0omnd 32132 nn0archi 32134 fermltlchr 32149 znfermltl 32150 ccfldextrr 32328 lmatfvlem 32387 rmulccn 32500 rrhre 32593 sigaex 32700 br2base 32860 sxbrsigalem3 32863 carsgclctunlem3 32911 sitmcl 32942 rpsqrtcn 33197 hgt750lem 33255 hgt750lem2 33256 afsval 33275 kur14lem7 33797 retopsconn 33834 satfvsuclem1 33944 fmlasuc0 33969 hfuni 34760 neibastop2lem 34823 onint1 34912 bj-snfromadj 35506 topdifinffinlem 35809 poimirlem9 36078 poimirlem28 36097 poimirlem30 36099 poimirlem32 36101 ftc1cnnc 36141 cncfres 36215 lineset 38192 lautset 38536 pautsetN 38552 tendoset 39213 decpmulnc 40779 decpmul 40780 areaquad 41528 0no 41689 finonex 41708 sblpnf 42572 lhe4.4ex1a 42591 fourierdlem62 44381 fourierdlem76 44395 65537prm 45740 11gbo 45939 bgoldbtbndlem1 45969 seppcld 46934 |
Copyright terms: Public domain | W3C validator |