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

Metamath Proof Explorer

Theorem vtocld

Description: Implicit substitution of a class for a setvar variable. (Contributed by Mario Carneiro, 15-Oct-2016) Avoid ax-10 , ax-11 , ax-12 . (Revised by SN, 2-Sep-2024)

Ref Expression
Hypotheses vtocld.1 
|- ( ph -> A e. V )
vtocld.2 
|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
vtocld.3 
|- ( ph -> ps )
Assertion vtocld 
|- ( ph -> ch )

Proof

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 elisset 
 |-  ( A e. V -> E. x x = A )
5 1 4 syl 
 |-  ( ph -> E. x x = A )
6 3 adantr 
 |-  ( ( ph /\ x = A ) -> ps )
7 6 2 mpbid 
 |-  ( ( ph /\ x = A ) -> ch )
8 5 7 exlimddv 
 |-  ( ph -> ch )