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

Proof

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