Metamath Proof Explorer


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 )