Theorem goaleq12d

Description: Equality of the "Godel-set of universal quantification". (Contributed by AV, 18-Sep-2023)

	Ref	Expression
Hypotheses	goaleq12d.1	|- ( ph -> M = N )
	goaleq12d.2	|- ( ph -> A = B )
Assertion	goaleq12d	|- ( ph -> A.g M A = A.g N B )

Proof

Step	Hyp	Ref	Expression
1		goaleq12d.1	|- ( ph -> M = N )
2		goaleq12d.2	|- ( ph -> A = B )
3		df-goal	|- A.g M A = <. 2o , <. M , A >. >.
4	3	a1i	|- ( ph -> A.g M A = <. 2o , <. M , A >. >. )
5	1 2	opeq12d	|- ( ph -> <. M , A >. = <. N , B >. )
6	5	opeq2d	|- ( ph -> <. 2o , <. M , A >. >. = <. 2o , <. N , B >. >. )
7		df-goal	|- A.g N B = <. 2o , <. N , B >. >.
8	7	eqcomi	|- <. 2o , <. N , B >. >. = A.g N B
9	8	a1i	|- ( ph -> <. 2o , <. N , B >. >. = A.g N B )
10	6 9	eqtrd	|- ( ph -> <. 2o , <. M , A >. >. = A.g N B )
11	4 10	eqtrd	|- ( ph -> A.g M A = A.g N B )