Theorem f1cnvcnv

Description: Two ways to express that a set A (not necessarily a function) is one-to-one. Each side is equivalent to Definition 6.4(3) of TakeutiZaring p. 24, who use the notation "Un_2 (A)" for one-to-one. We do not introduce a separate notation since we rarely use it. (Contributed by NM, 13-Aug-2004)

	Ref	Expression
Assertion	f1cnvcnv	|- ( `' `' A : dom A -1-1-> _V <-> ( Fun `' A /\ Fun `' `' A ) )

Proof

Step	Hyp	Ref	Expression
1		df-f1	|- ( `' `' A : dom A -1-1-> _V <-> ( `' `' A : dom A --> _V /\ Fun `' `' `' A ) )
2		dffn2	|- ( `' `' A Fn dom A <-> `' `' A : dom A --> _V )
3		dmcnvcnv	|- dom `' `' A = dom A
4		df-fn	|- ( `' `' A Fn dom A <-> ( Fun `' `' A /\ dom `' `' A = dom A ) )
5	3 4	mpbiran2	|- ( `' `' A Fn dom A <-> Fun `' `' A )
6	2 5	bitr3i	|- ( `' `' A : dom A --> _V <-> Fun `' `' A )
7		relcnv	|- Rel `' A
8		dfrel2	|- ( Rel `' A <-> `' `' `' A = `' A )
9	7 8	mpbi	|- `' `' `' A = `' A
10	9	funeqi	|- ( Fun `' `' `' A <-> Fun `' A )
11	6 10	anbi12ci	|- ( ( `' `' A : dom A --> _V /\ Fun `' `' `' A ) <-> ( Fun `' A /\ Fun `' `' A ) )
12	1 11	bitri	|- ( `' `' A : dom A -1-1-> _V <-> ( Fun `' A /\ Fun `' `' A ) )