Theorem elunirnALT

Description: Alternate proof of elunirn . It is shorter but requires ax-pow (through eluniima , funiunfv , ndmfv ). (Contributed by NM, 24-Sep-2006) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elunirnALT	|- ( Fun F -> ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) )

Proof

Step	Hyp	Ref	Expression
1		imadmrn	|- ( F " dom F ) = ran F
2	1	unieqi	|- U. ( F " dom F ) = U. ran F
3	2	eleq2i	|- ( A e. U. ( F " dom F ) <-> A e. U. ran F )
4		eluniima	|- ( Fun F -> ( A e. U. ( F " dom F ) <-> E. x e. dom F A e. ( F ` x ) ) )
5	3 4	bitr3id	|- ( Fun F -> ( A e. U. ran F <-> E. x e. dom F A e. ( F ` x ) ) )