Theorem vtoclegft

Description: Implicit substitution of a class for a setvar variable. (Closed theorem version of vtoclef .) (Contributed by NM, 7-Nov-2005) (Revised by Mario Carneiro, 11-Oct-2016) (Proof shortened by Wolf Lammen, 26-Jan-2025)

	Ref	Expression
Assertion	vtoclegft	|- ( ( A e. B /\ F/ x ph /\ A. x ( x = A -> ph ) ) -> ph )

Proof

Step	Hyp	Ref	Expression
1		biidd	|- ( x = A -> ( ph <-> ph ) )
2	1	ax-gen	|- A. x ( x = A -> ( ph <-> ph ) )
3		ceqsalt	|- ( ( F/ x ph /\ A. x ( x = A -> ( ph <-> ph ) ) /\ A e. B ) -> ( A. x ( x = A -> ph ) <-> ph ) )
4	2 3	mp3an2	|- ( ( F/ x ph /\ A e. B ) -> ( A. x ( x = A -> ph ) <-> ph ) )
5	4	ancoms	|- ( ( A e. B /\ F/ x ph ) -> ( A. x ( x = A -> ph ) <-> ph ) )
6	5	biimpd	|- ( ( A e. B /\ F/ x ph ) -> ( A. x ( x = A -> ph ) -> ph ) )
7	6	3impia	|- ( ( A e. B /\ F/ x ph /\ A. x ( x = A -> ph ) ) -> ph )