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

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 ⊢ Fun ⁡ A -1 -1 ↔ ∀ x ∃* y x A y

Proof

Step Hyp Ref Expression
1 funcnv2 ⊢ Fun ⁡ A -1 -1 ↔ ∀ x ∃* y y A -1 x
2 vex ⊢ y ∈ V
3 vex ⊢ x ∈ V
4 2 3 brcnv ⊢ y A -1 x ↔ x A y
5 4 mobii ⊢ ∃* y y A -1 x ↔ ∃* y x A y
6 5 albii ⊢ ∀ x ∃* y y A -1 x ↔ ∀ x ∃* y x A y
7 1 6 bitri ⊢ Fun ⁡ A -1 -1 ↔ ∀ x ∃* y x A y