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

Metamath Proof Explorer

Theorem vtocl3g

Description: Implicit substitution of a class for a setvar variable. Version of vtocl3gf with disjoint variable conditions instead of nonfreeness hypotheses, requiring fewer axioms. (Contributed by GG, 3-Oct-2024)

Ref Expression
Hypotheses vtocl3g.1 
|- ( x = A -> ( ph <-> ps ) )
vtocl3g.2 
|- ( y = B -> ( ps <-> ch ) )
vtocl3g.3 
|- ( z = C -> ( ch <-> th ) )
vtocl3g.4 
|- ph
Assertion vtocl3g 
|- ( ( A e. V /\ B e. W /\ C e. X ) -> th )

Proof

Step Hyp Ref Expression
1 vtocl3g.1 
 |-  ( x = A -> ( ph <-> ps ) )
2 vtocl3g.2 
 |-  ( y = B -> ( ps <-> ch ) )
3 vtocl3g.3 
 |-  ( z = C -> ( ch <-> th ) )
4 vtocl3g.4 
 |-  ph
5 elex 
 |-  ( A e. V -> A e. _V )
6 2 imbi2d 
 |-  ( y = B -> ( ( A e. _V -> ps ) <-> ( A e. _V -> ch ) ) )
7 3 imbi2d 
 |-  ( z = C -> ( ( A e. _V -> ch ) <-> ( A e. _V -> th ) ) )
8 1 4 vtoclg 
 |-  ( A e. _V -> ps )
9 6 7 8 vtocl2g 
 |-  ( ( B e. W /\ C e. X ) -> ( A e. _V -> th ) )
10 5 9 mpan9 
 |-  ( ( A e. V /\ ( B e. W /\ C e. X ) ) -> th )
11 10 3impb 
 |-  ( ( A e. V /\ B e. W /\ C e. X ) -> th )