This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funcnv2

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

Ref Expression
Assertion funcnv2 ⊢ Fun ⁡ A -1 ↔ ∀ y ∃* x x A y

Proof

Step Hyp Ref Expression
1 relcnv ⊢ Rel ⁡ A -1
2 dffun6 ⊢ Fun ⁡ A -1 ↔ Rel ⁡ A -1 ∧ ∀ y ∃* x y A -1 x
3 1 2 mpbiran ⊢ Fun ⁡ A -1 ↔ ∀ y ∃* x y A -1 x
4 vex ⊢ y ∈ V
5 vex ⊢ x ∈ V
6 4 5 brcnv ⊢ y A -1 x ↔ x A y
7 6 mobii ⊢ ∃* x y A -1 x ↔ ∃* x x A y
8 7 albii ⊢ ∀ y ∃* x y A -1 x ↔ ∀ y ∃* x x A y
9 3 8 bitri ⊢ Fun ⁡ A -1 ↔ ∀ y ∃* x x A y