![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > csbied | Structured version Unicode version |
Description: Conversion of implicit substitution to explicit substitution into a class. (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Mario Carneiro, 13-Oct-2016.) |
Ref | Expression |
---|---|
csbied.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
csbied.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
csbied |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1674 |
. 2
![]() ![]() ![]() ![]() | |
2 | nfcvd 2614 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | csbied.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | csbied.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 1, 2, 3, 4 | csbiedf 3409 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-v 3072 df-sbc 3287 df-csb 3389 |
This theorem is referenced by: csbied2 3415 fvmptd 5880 cantnfval 7979 cantnfvalOLD 8009 imasval 14553 gsumvalx 15606 mulgfval 15732 isga 15913 symgval 15988 gexval 16183 isirred 16899 psrval 17537 mplval 17610 opsrval 17665 evlsval 17714 evls1fval 17865 evl1fval 17873 znval 18077 tsmsval2 19818 dvfsumle 21611 dvfsumabs 21613 dvfsumlem1 21616 dvfsum2 21624 itgparts 21637 q1pval 21743 r1pval 21746 rlimcnp2 22478 vmaval 22569 fsumdvdscom 22643 fsumvma 22670 logexprlim 22682 dchrval 22691 dchrisumlema 22855 dchrisumlem2 22857 dchrisumlem3 22858 ttgval 23258 fprodeq0 27622 mendval 29680 mpt2sn 30863 telescfzgsumis 30954 telescfzgsum0is 30956 ply1mulgsumlem3 30990 ply1mulgsumlem4 30991 ply1mulgsum 30992 pmatcollpwfsupp 31231 pmatcollpw4 31242 pmatcollpw4fi 31243 pmattomply1mhmlem0 31274 pmattomply1mhmlem1 31275 pmattomply1mhmlem2 31276 chfacffsupp 31312 fsumshftd 32910 fsumshftdOLD 32911 hlhilset 35890 |
Copyright terms: Public domain | W3C validator |