Theorem eqeng

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

	Ref	Expression
Assertion	eqeng	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		enrefg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ≈ 𝐴 )
2		breq2	⊢ ( 𝐴 = 𝐵 → ( 𝐴 ≈ 𝐴 ↔ 𝐴 ≈ 𝐵 ) )
3	1 2	syl5ibcom	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐴 ≈ 𝐵 ) )