Theorem funcnv2

Description: A simpler equivalence for single-rooted (see funcnv ). (Contributed by NM, 9-Aug-2004)

	Ref	Expression
Assertion	funcnv2	|- ( Fun `' A <-> A. y E* x x A y )

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' A
2		dffun6	|- ( Fun `' A <-> ( Rel `' A /\ A. y E* x y `' A x ) )
3	1 2	mpbiran	|- ( Fun `' A <-> A. y E* x y `' A x )
4		vex	|- y e. _V
5		vex	|- x e. _V
6	4 5	brcnv	|- ( y `' A x <-> x A y )
7	6	mobii	|- ( E* x y `' A x <-> E* x x A y )
8	7	albii	|- ( A. y E* x y `' A x <-> A. y E* x x A y )
9	3 8	bitri	|- ( Fun `' A <-> A. y E* x x A y )