Theorem en2i

Description: Equinumerosity inference from an implicit one-to-one onto function. (Contributed by NM, 4-Jan-2004)

	Ref	Expression
Hypotheses	en2i.1	$$⊢A\in \mathrm{V}$$
	en2i.2	$$⊢B\in \mathrm{V}$$
	en2i.3	$$⊢x\in A\to C\in \mathrm{V}$$
	en2i.4	$$⊢y\in B\to D\in \mathrm{V}$$
	en2i.5	$$⊢\left(x\in A\wedge y=C\right)\leftrightarrow \left(y\in B\wedge x=D\right)$$
Assertion	en2i	$$⊢A\approx B$$

Proof

Step	Hyp	Ref	Expression
1		en2i.1	$$⊢A\in \mathrm{V}$$
2		en2i.2	$$⊢B\in \mathrm{V}$$
3		en2i.3	$$⊢x\in A\to C\in \mathrm{V}$$
4		en2i.4	$$⊢y\in B\to D\in \mathrm{V}$$
5		en2i.5	$$⊢\left(x\in A\wedge y=C\right)\leftrightarrow \left(y\in B\wedge x=D\right)$$
6	1	a1i	$$⊢\top \to A\in \mathrm{V}$$
7	2	a1i	$$⊢\top \to B\in \mathrm{V}$$
8	3	a1i	$$⊢\top \to \left(x\in A\to C\in \mathrm{V}\right)$$
9	4	a1i	$$⊢\top \to \left(y\in B\to D\in \mathrm{V}\right)$$
10	5	a1i	$$⊢\top \to \left(\left(x\in A\wedge y=C\right)\leftrightarrow \left(y\in B\wedge x=D\right)\right)$$
11	6 7 8 9 10	en2d	$$⊢\top \to A\approx B$$
12	11	mptru	$$⊢A\approx B$$