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 xYyYxHy=xGy
Assertion issubgoilem AYBYAHB=AGB

Proof

Step Hyp Ref Expression
1 issubgoilem.1 xYyYxHy=xGy
2 oveq1 x=AxHy=AHy
3 oveq1 x=AxGy=AGy
4 2 3 eqeq12d x=AxHy=xGyAHy=AGy
5 oveq2 y=BAHy=AHB
6 oveq2 y=BAGy=AGB
7 5 6 eqeq12d y=BAHy=AGyAHB=AGB
8 4 7 1 vtocl2ga AYBYAHB=AGB