# Metamath Proof Explorer

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

### Proof

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