Theorem enen2

Description: Equality-like theorem for equinumerosity. (Contributed by NM, 18-Dec-2003)

	Ref	Expression
Assertion	enen2	|- ( A ~~ B -> ( C ~~ A <-> C ~~ B ) )

Proof

Step	Hyp	Ref	Expression
1		entr	|- ( ( C ~~ A /\ A ~~ B ) -> C ~~ B )
2	1	ancoms	|- ( ( A ~~ B /\ C ~~ A ) -> C ~~ B )
3		ensym	|- ( A ~~ B -> B ~~ A )
4		entr	|- ( ( C ~~ B /\ B ~~ A ) -> C ~~ A )
5	4	ancoms	|- ( ( B ~~ A /\ C ~~ B ) -> C ~~ A )
6	3 5	sylan	|- ( ( A ~~ B /\ C ~~ B ) -> C ~~ A )
7	2 6	impbida	|- ( A ~~ B -> ( C ~~ A <-> C ~~ B ) )