Theorem funcnvsn

Description: The converse singleton of an ordered pair is a function. This is equivalent to funsn via cnvsn , but stating it this way allows to skip the sethood assumptions on A and B . (Contributed by NM, 30-Apr-2015)

	Ref	Expression
Assertion	funcnvsn	|- Fun `' { <. A , B >. }

Proof

Step	Hyp	Ref	Expression
1		relcnv	|- Rel `' { <. A , B >. }
2		moeq	|- E* y y = A
3		vex	|- x e. _V
4		vex	|- y e. _V
5	3 4	brcnv	|- ( x `' { <. A , B >. } y <-> y { <. A , B >. } x )
6		df-br	|- ( y { <. A , B >. } x <-> <. y , x >. e. { <. A , B >. } )
7	5 6	bitri	|- ( x `' { <. A , B >. } y <-> <. y , x >. e. { <. A , B >. } )
8		elsni	|- ( <. y , x >. e. { <. A , B >. } -> <. y , x >. = <. A , B >. )
9	4 3	opth1	|- ( <. y , x >. = <. A , B >. -> y = A )
10	8 9	syl	|- ( <. y , x >. e. { <. A , B >. } -> y = A )
11	7 10	sylbi	|- ( x `' { <. A , B >. } y -> y = A )
12	11	moimi	|- ( E* y y = A -> E* y x `' { <. A , B >. } y )
13	2 12	ax-mp	|- E* y x `' { <. A , B >. } y
14	13	ax-gen	|- A. x E* y x `' { <. A , B >. } y
15		dffun6	|- ( Fun `' { <. A , B >. } <-> ( Rel `' { <. A , B >. } /\ A. x E* y x `' { <. A , B >. } y ) )
16	1 14 15	mpbir2an	|- Fun `' { <. A , B >. }