Description: Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vtocld.1 | |- ( ph -> A e. V ) |
|
vtocld.2 | |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
||
vtocld.3 | |- ( ph -> ps ) |
||
Assertion | vtocld | |- ( ph -> ch ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vtocld.1 | |- ( ph -> A e. V ) |
|
2 | vtocld.2 | |- ( ( ph /\ x = A ) -> ( ps <-> ch ) ) |
|
3 | vtocld.3 | |- ( ph -> ps ) |
|
4 | nfv | |- F/ x ph |
|
5 | nfcvd | |- ( ph -> F/_ x A ) |
|
6 | nfvd | |- ( ph -> F/ x ch ) |
|
7 | 1 2 3 4 5 6 | vtocldf | |- ( ph -> ch ) |