Theorem enfi

Description: Equinumerous sets have the same finiteness. (Contributed by NM, 22-Aug-2008)

	Ref	Expression
Assertion	enfi	|- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )

Proof

Step	Hyp	Ref	Expression
1		enen1	|- ( A ~~ B -> ( A ~~ x <-> B ~~ x ) )
2	1	rexbidv	|- ( A ~~ B -> ( E. x e. _om A ~~ x <-> E. x e. _om B ~~ x ) )
3		isfi	|- ( A e. Fin <-> E. x e. _om A ~~ x )
4		isfi	|- ( B e. Fin <-> E. x e. _om B ~~ x )
5	2 3 4	3bitr4g	|- ( A ~~ B -> ( A e. Fin <-> B e. Fin ) )