Metamath Proof Explorer


Theorem funcnv2

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

Ref Expression
Assertion funcnv2 FunA-1y*xxAy

Proof

Step Hyp Ref Expression
1 relcnv RelA-1
2 dffun6 FunA-1RelA-1y*xyA-1x
3 1 2 mpbiran FunA-1y*xyA-1x
4 vex yV
5 vex xV
6 4 5 brcnv yA-1xxAy
7 6 mobii *xyA-1x*xxAy
8 7 albii y*xyA-1xy*xxAy
9 3 8 bitri FunA-1y*xxAy