Theorem funcnv2

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

	Ref	Expression
Assertion	funcnv2	$$⊢\mathrm{Fun}{A}^{-1}\leftrightarrow \forall y{\exists }^{*}xxAy$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
2		dffun6	$$⊢\mathrm{Fun}{A}^{-1}\leftrightarrow \left(\mathrm{Rel}{A}^{-1}\wedge \forall y{\exists }^{*}xy{A}^{-1}x\right)$$
3	1 2	mpbiran	$$⊢\mathrm{Fun}{A}^{-1}\leftrightarrow \forall y{\exists }^{*}xy{A}^{-1}x$$
4		vex	$$⊢y\in \mathrm{V}$$
5		vex	$$⊢x\in \mathrm{V}$$
6	4 5	brcnv	$$⊢y{A}^{-1}x\leftrightarrow xAy$$
7	6	mobii	$$⊢{\exists }^{*}xy{A}^{-1}x\leftrightarrow {\exists }^{*}xxAy$$
8	7	albii	$$⊢\forall y{\exists }^{*}xy{A}^{-1}x\leftrightarrow \forall y{\exists }^{*}xxAy$$
9	3 8	bitri	$$⊢\mathrm{Fun}{A}^{-1}\leftrightarrow \forall y{\exists }^{*}xxAy$$