Theorem goaleq12d

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

	Ref	Expression
Hypotheses	goaleq12d.1	⊢ ( 𝜑 → 𝑀 = 𝑁 )
	goaleq12d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion	goaleq12d	⊢ ( 𝜑 → ∀𝑔 𝑀 𝐴 = ∀𝑔 𝑁 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		goaleq12d.1	⊢ ( 𝜑 → 𝑀 = 𝑁 )
2		goaleq12d.2	⊢ ( 𝜑 → 𝐴 = 𝐵 )
3		df-goal	⊢ ∀𝑔 𝑀 𝐴 = ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩
4	3	a1i	⊢ ( 𝜑 → ∀𝑔 𝑀 𝐴 = ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩ )
5	1 2	opeq12d	⊢ ( 𝜑 → ⟨ 𝑀 , 𝐴 ⟩ = ⟨ 𝑁 , 𝐵 ⟩ )
6	5	opeq2d	⊢ ( 𝜑 → ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩ )
7		df-goal	⊢ ∀𝑔 𝑁 𝐵 = ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩
8	7	eqcomi	⊢ ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩ = ∀𝑔 𝑁 𝐵
9	8	a1i	⊢ ( 𝜑 → ⟨ 2o , ⟨ 𝑁 , 𝐵 ⟩ ⟩ = ∀𝑔 𝑁 𝐵 )
10	6 9	eqtrd	⊢ ( 𝜑 → ⟨ 2o , ⟨ 𝑀 , 𝐴 ⟩ ⟩ = ∀𝑔 𝑁 𝐵 )
11	4 10	eqtrd	⊢ ( 𝜑 → ∀𝑔 𝑀 𝐴 = ∀𝑔 𝑁 𝐵 )