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 ) )