Theorem goaleq12d

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

	Ref	Expression
Hypotheses	goaleq12d.1	$$⊢\phi \to M=N$$
	goaleq12d.2	$$⊢\phi \to A=B$$
Assertion	goaleq12d	$$⊢\phi \to \left[{\forall }_{𝑔}MA\right]=\left[{\forall }_{𝑔}NB\right]$$

Proof

Step	Hyp	Ref	Expression
1		goaleq12d.1	$$⊢\phi \to M=N$$
2		goaleq12d.2	$$⊢\phi \to A=B$$
3		df-goal	$$⊢\left[{\forall }_{𝑔}MA\right]=⟨2_{𝑜},⟨M,A⟩⟩$$
4	3	a1i	$$⊢\phi \to \left[{\forall }_{𝑔}MA\right]=⟨2_{𝑜},⟨M,A⟩⟩$$
5	1 2	opeq12d	$$⊢\phi \to ⟨M,A⟩=⟨N,B⟩$$
6	5	opeq2d	$$⊢\phi \to ⟨2_{𝑜},⟨M,A⟩⟩=⟨2_{𝑜},⟨N,B⟩⟩$$
7		df-goal	$$⊢\left[{\forall }_{𝑔}NB\right]=⟨2_{𝑜},⟨N,B⟩⟩$$
8	7	eqcomi	$$⊢⟨2_{𝑜},⟨N,B⟩⟩=\left[{\forall }_{𝑔}NB\right]$$
9	8	a1i	$$⊢\phi \to ⟨2_{𝑜},⟨N,B⟩⟩=\left[{\forall }_{𝑔}NB\right]$$
10	6 9	eqtrd	$$⊢\phi \to ⟨2_{𝑜},⟨M,A⟩⟩=\left[{\forall }_{𝑔}NB\right]$$
11	4 10	eqtrd	$$⊢\phi \to \left[{\forall }_{𝑔}MA\right]=\left[{\forall }_{𝑔}NB\right]$$