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 e. _V
	en3i.2	|- B e. _V
	en3i.3	|- ( x e. A -> C e. B )
	en3i.4	|- ( y e. B -> D e. A )
	en3i.5	|- ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) )
Assertion	en3i	|- A ~~ B

Proof

Step	Hyp	Ref	Expression
1		en3i.1	|- A e. _V
2		en3i.2	|- B e. _V
3		en3i.3	|- ( x e. A -> C e. B )
4		en3i.4	|- ( y e. B -> D e. A )
5		en3i.5	|- ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) )
6	1	a1i	|- ( T. -> A e. _V )
7	2	a1i	|- ( T. -> B e. _V )
8	3	a1i	|- ( T. -> ( x e. A -> C e. B ) )
9	4	a1i	|- ( T. -> ( y e. B -> D e. A ) )
10	5	a1i	|- ( T. -> ( ( x e. A /\ y e. B ) -> ( x = D <-> y = C ) ) )
11	6 7 8 9 10	en3d	|- ( T. -> A ~~ B )
12	11	mptru	|- A ~~ B