Theorem brdom

Description: Dominance relation. (Contributed by NM, 15-Jun-1998)

	Ref	Expression
Hypothesis	bren.1	|- B e. _V
Assertion	brdom	|- ( A ~<_ B <-> E. f f : A -1-1-> B )

Proof

Step	Hyp	Ref	Expression
1		bren.1	|- B e. _V
2		brdomg	|- ( B e. _V -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
3	1 2	ax-mp	|- ( A ~<_ B <-> E. f f : A -1-1-> B )