Theorem funop

Description: An ordered pair is a function iff it is a singleton of an ordered pair. (Contributed by AV, 20-Sep-2020) A function is a class of ordered pairs, so the fact that an ordered pair may sometimes be itself a function is an "accident" depending on the specific encoding of ordered pairs as classes (in set.mm, the Kuratowski encoding). A more meaningful statement is funsng , as relsnopg is to relop . (New usage is discouraged.)

	Ref	Expression
Hypotheses	funopsn.x	|- X e. _V
	funopsn.y	|- Y e. _V
Assertion	funop	|- ( Fun <. X , Y >. <-> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )

Proof

Step	Hyp	Ref	Expression
1		funopsn.x	|- X e. _V
2		funopsn.y	|- Y e. _V
3		eqid	|- <. X , Y >. = <. X , Y >.
4	1 2	funopsn	|- ( ( Fun <. X , Y >. /\ <. X , Y >. = <. X , Y >. ) -> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )
5	3 4	mpan2	|- ( Fun <. X , Y >. -> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )
6		vex	|- a e. _V
7	6 6	funsn	|- Fun { <. a , a >. }
8		funeq	|- ( <. X , Y >. = { <. a , a >. } -> ( Fun <. X , Y >. <-> Fun { <. a , a >. } ) )
9	7 8	mpbiri	|- ( <. X , Y >. = { <. a , a >. } -> Fun <. X , Y >. )
10	9	adantl	|- ( ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) -> Fun <. X , Y >. )
11	10	exlimiv	|- ( E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) -> Fun <. X , Y >. )
12	5 11	impbii	|- ( Fun <. X , Y >. <-> E. a ( X = { a } /\ <. X , Y >. = { <. a , a >. } ) )