Metamath Proof Explorer

Theorem en2d

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 27-Jul-2004) (Revised by Mario Carneiro, 12-May-2014) (Revised by AV, 4-Aug-2024)

		Ref	Expression
	Hypotheses	en2d.1	$⊢ φ \to A \in V$
		en2d.2	$⊢ φ \to B \in W$
		en2d.3	$⊢ φ \to (x \in A \to C \in X)$
		en2d.4	$⊢ φ \to (y \in B \to D \in Y)$
		en2d.5	$⊢ φ \to ((x \in A \land y = C) \leftrightarrow (y \in B \land x = D))$
	Assertion	en2d	$⊢ φ \to A \approx B$

Proof

Step	Hyp	Ref	Expression
1		en2d.1	$⊢ φ \to A \in V$
2		en2d.2	$⊢ φ \to B \in W$
3		en2d.3	$⊢ φ \to (x \in A \to C \in X)$
4		en2d.4	$⊢ φ \to (y \in B \to D \in Y)$
5		en2d.5	$⊢ φ \to ((x \in A \land y = C) \leftrightarrow (y \in B \land x = D))$
6		eqid	$⊢ (x \in A ⟼ C) = (x \in A ⟼ C)$
7	3	imp	$⊢ (φ \land x \in A) \to C \in X$
8	4	imp	$⊢ (φ \land y \in B) \to D \in Y$
9	6 7 8 5	f1od	$⊢ φ \to (x \in A ⟼ C) : A \underset{1-1 onto}{⟶} B$
10		f1oen2g	$⊢ (A \in V \land B \in W \land (x \in A ⟼ C) : A \underset{1-1 onto}{⟶} B) \to A \approx B$
11	1 2 9 10	syl3anc	$⊢ φ \to A \approx B$