Theorem fun2cnv

Description: The double converse of a class is a function iff the class is single-valued. Each side is equivalent to Definition 6.4(2) of TakeutiZaring p. 23, who use the notation "Un(A)" for single-valued. Note that A is not necessarily a function. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	fun2cnv	$$⊢\mathrm{Fun}{A^{-1}}^{-1}\leftrightarrow \forall x{\exists }^{*}yxAy$$

Proof

Step	Hyp	Ref	Expression
1		funcnv2	$$⊢\mathrm{Fun}{A^{-1}}^{-1}\leftrightarrow \forall x{\exists }^{*}yy{A}^{-1}x$$
2		vex	$$⊢y\in \mathrm{V}$$
3		vex	$$⊢x\in \mathrm{V}$$
4	2 3	brcnv	$$⊢y{A}^{-1}x\leftrightarrow xAy$$
5	4	mobii	$$⊢{\exists }^{*}yy{A}^{-1}x\leftrightarrow {\exists }^{*}yxAy$$
6	5	albii	$$⊢\forall x{\exists }^{*}yy{A}^{-1}x\leftrightarrow \forall x{\exists }^{*}yxAy$$
7	1 6	bitri	$$⊢\mathrm{Fun}{A^{-1}}^{-1}\leftrightarrow \forall x{\exists }^{*}yxAy$$