Theorem eqidd

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

	Ref	Expression
Assertion	eqidd	⊢ ( 𝜑 → 𝐴 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ 𝐴 = 𝐴
2	1	a1i	⊢ ( 𝜑 → 𝐴 = 𝐴 )