Theorem bren2

Description: Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	bren2	|- ( A ~~ B <-> ( A ~<_ B /\ -. A ~< B ) )

Proof

Step	Hyp	Ref	Expression
1		endom	|- ( A ~~ B -> A ~<_ B )
2		sdomnen	|- ( A ~< B -> -. A ~~ B )
3	2	con2i	|- ( A ~~ B -> -. A ~< B )
4	1 3	jca	|- ( A ~~ B -> ( A ~<_ B /\ -. A ~< B ) )
5		brdom2	|- ( A ~<_ B <-> ( A ~< B \/ A ~~ B ) )
6	5	biimpi	|- ( A ~<_ B -> ( A ~< B \/ A ~~ B ) )
7	6	orcanai	|- ( ( A ~<_ B /\ -. A ~< B ) -> A ~~ B )
8	4 7	impbii	|- ( A ~~ B <-> ( A ~<_ B /\ -. A ~< B ) )