![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > syl6eqelr | Structured version Visualization version GIF version |
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.) |
Ref | Expression |
---|---|
syl6eqelr.1 | ⊢ (𝜑 → 𝐵 = 𝐴) |
syl6eqelr.2 | ⊢ 𝐵 ∈ 𝐶 |
Ref | Expression |
---|---|
syl6eqelr | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6eqelr.1 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐴) | |
2 | 1 | eqcomd 2657 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
3 | syl6eqelr.2 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
4 | 2, 3 | syl6eqel 2738 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ∈ wcel 2030 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1745 df-cleq 2644 df-clel 2647 |
This theorem is referenced by: wemoiso2 7196 releldm2 7262 mapprc 7903 ixpprc 7971 bren 8006 brdomg 8007 ctex 8012 domssex 8162 mapen 8165 ssenen 8175 fodomfib 8281 fi0 8367 dffi3 8378 brwdom 8513 brwdomn0 8515 unxpwdom2 8534 ixpiunwdom 8537 tcmin 8655 rankonid 8730 rankr1id 8763 cardf2 8807 cardid2 8817 carduni 8845 fseqen 8888 acndom 8912 acndom2 8915 alephnbtwn 8932 cardcf 9112 cfeq0 9116 cflim2 9123 coftr 9133 infpssr 9168 hsmexlem5 9290 axdc3lem4 9313 fodomb 9386 ondomon 9423 gruina 9678 ioof 12309 hashbc 13275 hashfacen 13276 trclun 13799 zsum 14493 fsum 14495 fsumcom2OLD 14550 fprod 14715 fprodcom2OLD 14759 xpsfrnel2 16272 eqgen 17694 symgbas 17846 symgfisg 17934 dvdsr 18692 asplss 19377 aspsubrg 19379 psrval 19410 clsf 20900 restco 21016 subbascn 21106 is2ndc 21297 ptbasin2 21429 ptbas 21430 indishmph 21649 ufldom 21813 cnextfres1 21919 ussid 22111 icopnfcld 22618 cnrehmeo 22799 csscld 23094 clsocv 23095 itg2gt0 23572 dvmptadd 23768 dvmptmul 23769 dvmptco 23780 logcn 24438 selberglem1 25279 hmopidmchi 29138 sigagensiga 30332 dya2iocbrsiga 30465 dya2icobrsiga 30466 logdivsqrle 30856 fnessref 32477 unirep 33637 indexdom 33659 dicfnN 36789 pwslnmlem0 37978 mendval 38070 icof 39725 dvsubf 40446 dvdivf 40455 itgsinexplem1 40487 stirlinglem7 40615 fourierdlem73 40714 fouriersw 40766 ovolval4lem1 41184 |
Copyright terms: Public domain | W3C validator |