Theorem dfdm4

Description: Alternate definition of domain. (Contributed by NM, 28-Dec-1996)

	Ref	Expression
Assertion	dfdm4	|- dom A = ran `' A

Proof

Step	Hyp	Ref	Expression
1		vex	|- y e. _V
2		vex	|- x e. _V
3	1 2	brcnv	|- ( y `' A x <-> x A y )
4	3	exbii	|- ( E. y y `' A x <-> E. y x A y )
5	4	abbii	|- { x | E. y y `' A x } = { x | E. y x A y }
6		dfrn2	|- ran `' A = { x | E. y y `' A x }
7		df-dm	|- dom A = { x | E. y x A y }
8	5 6 7	3eqtr4ri	|- dom A = ran `' A