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 ^◡ ^◡ 𝐴 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 )

Proof

Step	Hyp	Ref	Expression
1		funcnv2	⊢ ( Fun ^◡ ^◡ 𝐴 ↔ ∀ 𝑥 ∃* 𝑦 𝑦 ^◡ 𝐴 𝑥 )
2		vex	⊢ 𝑦 ∈ V
3		vex	⊢ 𝑥 ∈ V
4	2 3	brcnv	⊢ ( 𝑦 ^◡ 𝐴 𝑥 ↔ 𝑥 𝐴 𝑦 )
5	4	mobii	⊢ ( ∃* 𝑦 𝑦 ^◡ 𝐴 𝑥 ↔ ∃* 𝑦 𝑥 𝐴 𝑦 )
6	5	albii	⊢ ( ∀ 𝑥 ∃* 𝑦 𝑦 ^◡ 𝐴 𝑥 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 )
7	1 6	bitri	⊢ ( Fun ^◡ ^◡ 𝐴 ↔ ∀ 𝑥 ∃* 𝑦 𝑥 𝐴 𝑦 )