This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem idssen

Description: Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998) (Revised by Mario Carneiro, 15-Nov-2014)

		Ref	Expression
	Assertion	idssen	$⊢ I \subseteq \approx$

Step	Hyp	Ref	Expression
1		reli	$⊢ Rel I$
2		vex	$⊢ y \in V$
3	2	ideq	$⊢ x I y \leftrightarrow x = y$
4		eqeng	$⊢ x \in V \to (x = y \to x \approx y)$
5	4	elv	$⊢ x = y \to x \approx y$
6	3 5	sylbi	$⊢ x I y \to x \approx y$
7		df-br	$⊢ x I y \leftrightarrow ⟨x, y⟩ \in I$
8		df-br	$⊢ x \approx y \leftrightarrow ⟨x, y⟩ \in \approx$
9	6 7 8	3imtr3i	$⊢ ⟨x, y⟩ \in I \to ⟨x, y⟩ \in \approx$
10	1 9	relssi	$⊢ I \subseteq \approx$