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

Metamath Proof Explorer

Theorem issubgoilem

Description: Lemma for hhssabloilem . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypothesis issubgoilem.1 
|- ( ( x e. Y /\ y e. Y ) -> ( x H y ) = ( x G y ) )
Assertion issubgoilem 
|- ( ( A e. Y /\ B e. Y ) -> ( A H B ) = ( A G B ) )

Proof

Step Hyp Ref Expression
1 issubgoilem.1 
 |-  ( ( x e. Y /\ y e. Y ) -> ( x H y ) = ( x G y ) )
2 oveq1 
 |-  ( x = A -> ( x H y ) = ( A H y ) )
3 oveq1 
 |-  ( x = A -> ( x G y ) = ( A G y ) )
4 2 3 eqeq12d 
 |-  ( x = A -> ( ( x H y ) = ( x G y ) <-> ( A H y ) = ( A G y ) ) )
5 oveq2 
 |-  ( y = B -> ( A H y ) = ( A H B ) )
6 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
7 5 6 eqeq12d 
 |-  ( y = B -> ( ( A H y ) = ( A G y ) <-> ( A H B ) = ( A G B ) ) )
8 4 7 1 vtocl2ga 
 |-  ( ( A e. Y /\ B e. Y ) -> ( A H B ) = ( A G B ) )