![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vtoclgaf | Structured version Visualization version Unicode version |
Description: Implicit substitution of a class for a setvar variable. (Contributed by NM, 17-Feb-2006.) (Revised by Mario Carneiro, 10-Oct-2016.) |
Ref | Expression |
---|---|
vtoclgaf.1 |
![]() ![]() ![]() ![]() |
vtoclgaf.2 |
![]() ![]() ![]() ![]() |
vtoclgaf.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
vtoclgaf.4 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
vtoclgaf |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtoclgaf.1 |
. . 3
![]() ![]() ![]() ![]() | |
2 | 1 | nfel1 2608 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() |
3 | vtoclgaf.2 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 2, 3 | nfim 2005 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | eleq1 2519 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | vtoclgaf.3 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 5, 6 | imbi12d 322 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | vtoclgaf.4 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
9 | 1, 4, 7, 8 | vtoclgf 3107 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
10 | 9 | pm2.43i 49 |
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 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2583 df-v 3049 |
This theorem is referenced by: vtoclga 3115 ssiun2s 4325 fvmptss 5963 fvmptf 5971 fmptco 6061 tfis 6686 inar1 9205 sumss 13802 fprodn0 14045 prmind2 14647 lss1d 18198 itg2splitlem 22718 dgrle 23209 cnlnadjlem5 27736 poimirlem25 31977 stoweidlem26 37896 iunopeqop 39015 |
Copyright terms: Public domain | W3C validator |