This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )