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 2824 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) |
3 | syl6eqelr.2 | . 2 ⊢ 𝐵 ∈ 𝐶 | |
4 | 2, 3 | syl6eqel 2918 | 1 ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = 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 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2811 df-clel 2890 |
This theorem is referenced by: wemoiso2 7664 releldm2 7731 mapprc 8399 ixpprc 8471 bren 8506 brdomg 8507 domssex 8666 mapen 8669 ssenen 8679 fodomfib 8786 fi0 8872 dffi3 8883 brwdom 9019 brwdomn0 9021 unxpwdom2 9040 ixpiunwdom 9043 tcmin 9171 rankonid 9246 rankr1id 9279 cardf2 9360 cardid2 9370 carduni 9398 fseqen 9441 acndom 9465 acndom2 9468 alephnbtwn 9485 cardcf 9662 cfeq0 9666 cflim2 9673 coftr 9683 infpssr 9718 hsmexlem5 9840 axdc3lem4 9863 fodomb 9936 ondomon 9973 gruina 10228 ioof 12823 hashbc 13799 hashfacen 13800 trclun 14362 zsum 15063 fsum 15065 fprod 15283 eqgen 18271 symgbas 18436 symgfisg 18525 dvdsr 19325 asplss 20031 aspsubrg 20033 psrval 20070 clsf 21584 restco 21700 subbascn 21790 is2ndc 21982 ptbasin2 22114 ptbas 22115 indishmph 22334 ufldom 22498 cnextfres1 22604 ussid 22796 icopnfcld 23303 cnrehmeo 23484 csscld 23779 clsocv 23780 itg2gt0 24288 dvmptadd 24484 dvmptmul 24485 dvmptco 24496 logcn 25157 selberglem1 26048 hmopidmchi 29855 sigagensiga 31299 dya2iocbrsiga 31432 dya2icobrsiga 31433 logdivsqrle 31820 fnessref 33602 unirep 34869 indexdom 34890 dicfnN 38199 pwslnmlem0 39569 mendval 39661 icof 41358 dvsubf 42074 dvdivf 42083 itgsinexplem1 42115 stirlinglem7 42242 fourierdlem73 42341 fouriersw 42393 ovolval4lem1 42808 |
Copyright terms: Public domain | W3C validator |