Theorem eqidd

Description: Class identity law with antecedent. (Contributed by NM, 21-Aug-2008)

	Ref	Expression
Assertion	eqidd	$$⊢\phi \to A=A$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A=A$$
2	1	a1i	$$⊢\phi \to A=A$$