This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )