![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclgf | Structured version Visualization version Unicode version |
Description: Implicit substitution of a class for a setvar variable, with bound-variable hypotheses in place of disjoint variable restrictions. (Contributed by NM, 21-Sep-2003.) (Proof shortened by Mario Carneiro, 10-Oct-2016.) |
Ref | Expression |
---|---|
vtoclgf.1 |
![]() ![]() ![]() ![]() |
vtoclgf.2 |
![]() ![]() ![]() ![]() |
vtoclgf.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtoclgf.4 |
![]() ![]() |
Ref | Expression |
---|---|
vtoclgf |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3053 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | vtoclgf.1 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | 2 | issetf 3049 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | vtoclgf.2 |
. . . 4
![]() ![]() ![]() ![]() | |
5 | vtoclgf.4 |
. . . . 5
![]() ![]() | |
6 | vtoclgf.3 |
. . . . 5
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | mpbii 215 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 4, 7 | exlimi 1994 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
9 | 3, 8 | sylbi 199 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 1, 9 | 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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-v 3046 |
This theorem is referenced by: vtocl2gf 3108 vtocl3gf 3109 vtoclgaf 3111 elabgf 3182 fprodsplit1f 14037 ssiun2sf 28167 subtr 30963 subtr2 30964 supxrgere 37550 supxrgelem 37554 supxrge 37555 fsumsplit1 37645 fmuldfeqlem1 37654 climsuse 37681 dvnmptdivc 37807 dvmptfprodlem 37813 stoweidlem59 37914 fourierdlem31 37994 fourierdlem31OLD 37995 sge0f1o 38218 sge0fodjrnlem 38252 |
Copyright terms: Public domain | W3C validator |