Theorem issubgoilem

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

	Ref	Expression
Hypothesis	issubgoilem.1	⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
Assertion	issubgoilem	⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		issubgoilem.1	⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐺 𝑦 ) )
2		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐻 𝑦 ) = ( 𝐴 𝐻 𝑦 ) )
3		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐺 𝑦 ) = ( 𝐴 𝐺 𝑦 ) )
4	2 3	eqeq12d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝐻 𝑦 ) = ( 𝑥 𝐺 𝑦 ) ↔ ( 𝐴 𝐻 𝑦 ) = ( 𝐴 𝐺 𝑦 ) ) )
5		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐻 𝑦 ) = ( 𝐴 𝐻 𝐵 ) )
6		oveq2	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 𝑦 ) = ( 𝐴 𝐺 𝐵 ) )
7	5 6	eqeq12d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝐻 𝑦 ) = ( 𝐴 𝐺 𝑦 ) ↔ ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐺 𝐵 ) ) )
8	4 7 1	vtocl2ga	⊢ ( ( 𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 𝐻 𝐵 ) = ( 𝐴 𝐺 𝐵 ) )