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

Metamath Proof Explorer

Theorem vtocl2g

Description: Implicit substitution of 2 classes for 2 setvar variables. (Contributed by NM, 25-Apr-1995) Remove dependency on ax-10 , ax-11 , and ax-13 . (Revised by Steven Nguyen, 29-Nov-2022)

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

Proof

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