Theorem eqeng

Description: Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003)

	Ref	Expression
Assertion	eqeng	$$⊢A\in V\to \left(A=B\to A\approx B\right)$$

Proof

Step	Hyp	Ref	Expression
1		enrefg	$$⊢A\in V\to A\approx A$$
2		breq2	$$⊢A=B\to \left(A\approx A\leftrightarrow A\approx B\right)$$
3	1 2	syl5ibcom	$$⊢A\in V\to \left(A=B\to A\approx B\right)$$