This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )