| 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 2746 | . 2 ⊢ 𝐵 = 𝐴 |
| 3 | eqeltrri.2 | . 2 ⊢ 𝐴 ∈ 𝐶 | |
| 4 | 2, 3 | eqeltri 2837 | 1 ⊢ 𝐵 ∈ 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: = 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: 3eltr3i 2853 zfrep4 5293 p0ex 5384 pp0ex 5386 ord3ex 5387 zfpair 5421 epse 5667 unexOLD 7765 fvresex 7984 opabex3 7992 abexssex 7995 abexex 7996 oprabrexex2 8003 seqomlem3 8492 1on 8518 2on 8520 inf0 9661 scottexs 9927 kardex 9934 infxpenlem 10053 r1om 10283 cfon 10295 fin23lem16 10375 fin1a2lem6 10445 hsmexlem5 10470 brdom7disj 10571 brdom6disj 10572 1lt2pi 10945 0cn 11253 resubcli 11571 0reALT 11606 1nn 12277 10nn 12749 numsucc 12773 nummac 12778 unirnioo 13489 ioorebas 13491 om2uzrani 13993 uzrdg0i 14000 hashunlei 14464 cats1fvn 14897 trclubi 15035 4sqlem19 17001 dec2dvds 17101 mod2xnegi 17109 modsubi 17110 gcdi 17111 isstruct2 17186 grppropstr 18971 nn0srg 21455 fermltlchr 21544 ltbval 22061 sn0topon 23005 indistop 23009 indisuni 23010 indistps2 23019 indistps2ALT 23022 restbas 23166 leordtval2 23220 iocpnfordt 23223 icomnfordt 23224 iooordt 23225 reordt 23226 dis1stc 23507 ptcmpfi 23821 ustfn 24210 ustn0 24229 retopbas 24781 blssioo 24816 xrtgioo 24828 zcld 24835 cnperf 24842 retopconn 24851 iimulcnOLD 24968 rembl 25575 mbfdm 25661 ismbf 25663 mbf0 25669 bddiblnc 25877 abelthlem9 26484 advlog 26696 advlogexp 26697 2irrexpq 26773 cxpcn3 26791 loglesqrt 26804 log2ub 26992 ppi1i 27211 cht2 27215 cht3 27216 bpos1lem 27326 lgslem4 27344 vmadivsum 27526 log2sumbnd 27588 selberg2 27595 selbergr 27612 nogt01o 27741 mulsproplem9 28150 1n0s 28351 2nns 28402 iscgrg 28520 ishpg 28767 ax5seglem7 28950 h2hva 30993 h2hsm 30994 h2hnm 30995 norm-ii-i 31156 hhshsslem2 31287 shincli 31381 chincli 31479 lnophdi 32021 imaelshi 32077 rnelshi 32078 bdophdi 32116 dfdec100 32832 dpadd2 32892 dpmul 32895 dpmul4 32896 nn0omnd 33373 nn0archi 33375 znfermltl 33394 ccfldextrr 33699 lmatfvlem 33814 rrhre 34022 sigaex 34111 br2base 34271 sxbrsigalem3 34274 carsgclctunlem3 34322 sitmcl 34353 rpsqrtcn 34608 hgt750lem 34666 hgt750lem2 34667 afsval 34686 kur14lem7 35217 retopsconn 35254 satfvsuclem1 35364 fmlasuc0 35389 hfuni 36185 neibastop2lem 36361 onint1 36450 bj-snfromadj 37045 topdifinffinlem 37348 poimirlem9 37636 poimirlem28 37655 poimirlem30 37657 poimirlem32 37659 ftc1cnnc 37699 cncfres 37772 lineset 39740 lautset 40084 pautsetN 40100 tendoset 40761 decpmulnc 42322 decpmul 42323 areaquad 43228 0no 43448 finonex 43467 sblpnf 44329 lhe4.4ex1a 44348 fourierdlem62 46183 fourierdlem76 46197 65537prm 47563 11gbo 47762 bgoldbtbndlem1 47792 seppcld 48827 |
| Copyright terms: Public domain | W3C validator |