Metamath Proof Explorer

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}↔\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$

Proof

Step Hyp Ref Expression
1 funcnv2 ${⊢}\mathrm{Fun}{{{A}}^{-1}}^{-1}↔\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}{{A}}^{-1}{x}$
2 vex ${⊢}{y}\in \mathrm{V}$
3 vex ${⊢}{x}\in \mathrm{V}$
4 2 3 brcnv ${⊢}{y}{{A}}^{-1}{x}↔{x}{A}{y}$
5 4 mobii ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}{{A}}^{-1}{x}↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{y}{{A}}^{-1}{x}↔\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$
7 1 6 bitri ${⊢}\mathrm{Fun}{{{A}}^{-1}}^{-1}↔\forall {x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{x}{A}{y}$