Theorem fisseneq

Description: A finite set is equal to its subset if they are equinumerous. (Contributed by FL, 11-Aug-2008)

	Ref	Expression
Assertion	fisseneq	|- ( ( B e. Fin /\ A C_ B /\ A ~~ B ) -> A = B )

Proof

Step	Hyp	Ref	Expression
1		df-pss	|- ( A C. B <-> ( A C_ B /\ A =/= B ) )
2		pssinf	|- ( ( A C. B /\ A ~~ B ) -> -. B e. Fin )
3	2	expcom	|- ( A ~~ B -> ( A C. B -> -. B e. Fin ) )
4	1 3	biimtrrid	|- ( A ~~ B -> ( ( A C_ B /\ A =/= B ) -> -. B e. Fin ) )
5	4	expdimp	|- ( ( A ~~ B /\ A C_ B ) -> ( A =/= B -> -. B e. Fin ) )
6	5	necon4ad	|- ( ( A ~~ B /\ A C_ B ) -> ( B e. Fin -> A = B ) )
7	6	3impia	|- ( ( A ~~ B /\ A C_ B /\ B e. Fin ) -> A = B )
8	7	3com13	|- ( ( B e. Fin /\ A C_ B /\ A ~~ B ) -> A = B )