![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclg1f | Structured version Visualization version Unicode version |
Description: Version of vtoclgf 3091 with one non-freeness hypothesis replaced with a dv condition, thus avoiding dependency on ax-11 1937 and ax-13 2104. (Contributed by BJ, 1-May-2019.) |
Ref | Expression |
---|---|
vtoclg1f.nf |
![]() ![]() ![]() ![]() |
vtoclg1f.maj |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtoclg1f.min |
![]() ![]() |
Ref | Expression |
---|---|
vtoclg1f |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3040 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | isset 3035 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | vtoclg1f.nf |
. . . 4
![]() ![]() ![]() ![]() | |
4 | vtoclg1f.min |
. . . . 5
![]() ![]() | |
5 | vtoclg1f.maj |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | 4, 5 | mpbii 216 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 3, 6 | exlimi 2015 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 2, 7 | sylbi 200 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 1, 8 | syl 17 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-12 1950 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-v 3033 |
This theorem is referenced by: vtoclg 3093 ceqsexg 3158 mob 3208 opeliunxp2 4978 fvopab5 5989 opeliunxp2f 6975 cnextfvval 21158 dvfsumlem2 23058 dvfsumlem4 23060 bnj981 29833 fmul01 37755 fmuldfeq 37758 fmul01lt1lem1 37759 cncfiooicclem1 37868 stoweidlem3 37975 stoweidlem26 37998 stoweidlem31 38004 stoweidlem43 38016 stoweidlem51 38024 fourierdlem86 38168 fourierdlem89 38171 fourierdlem91 38173 |
Copyright terms: Public domain | W3C validator |