Theorem en3i

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

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

Proof

Step	Hyp	Ref	Expression
1		en3i.1	$$⊢A\in \mathrm{V}$$
2		en3i.2	$$⊢B\in \mathrm{V}$$
3		en3i.3	$$⊢x\in A\to C\in B$$
4		en3i.4	$$⊢y\in B\to D\in A$$
5		en3i.5	$$⊢\left(x\in A\wedge y\in B\right)\to \left(x=D\leftrightarrow y=C\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 B\right)$$
9	4	a1i	$$⊢\top \to \left(y\in B\to D\in A\right)$$
10	5	a1i	$$⊢\top \to \left(\left(x\in A\wedge y\in B\right)\to \left(x=D\leftrightarrow y=C\right)\right)$$
11	6 7 8 9 10	en3d	$$⊢\top \to A\approx B$$
12	11	mptru	$$⊢A\approx B$$