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	⊢ ( ◡ ◡ 𝐴 : dom 𝐴 –1-1→ V ↔ ( Fun ◡ 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df-f1	⊢ ( ◡ ◡ 𝐴 : dom 𝐴 –1-1→ V ↔ ( ◡ ◡ 𝐴 : dom 𝐴 ⟶ V ∧ Fun ◡ ◡ ◡ 𝐴 ) )
2		dffn2	⊢ ( ◡ ◡ 𝐴 Fn dom 𝐴 ↔ ◡ ◡ 𝐴 : dom 𝐴 ⟶ V )
3		dmcnvcnv	⊢ dom ◡ ◡ 𝐴 = dom 𝐴
4		df-fn	⊢ ( ◡ ◡ 𝐴 Fn dom 𝐴 ↔ ( Fun ◡ ◡ 𝐴 ∧ dom ◡ ◡ 𝐴 = dom 𝐴 ) )
5	3 4	mpbiran2	⊢ ( ◡ ◡ 𝐴 Fn dom 𝐴 ↔ Fun ◡ ◡ 𝐴 )
6	2 5	bitr3i	⊢ ( ◡ ◡ 𝐴 : dom 𝐴 ⟶ V ↔ Fun ◡ ◡ 𝐴 )
7		relcnv	⊢ Rel ◡ 𝐴
8		dfrel2	⊢ ( Rel ◡ 𝐴 ↔ ◡ ◡ ◡ 𝐴 = ◡ 𝐴 )
9	7 8	mpbi	⊢ ◡ ◡ ◡ 𝐴 = ◡ 𝐴
10	9	funeqi	⊢ ( Fun ◡ ◡ ◡ 𝐴 ↔ Fun ◡ 𝐴 )
11	6 10	anbi12ci	⊢ ( ( ◡ ◡ 𝐴 : dom 𝐴 ⟶ V ∧ Fun ◡ ◡ ◡ 𝐴 ) ↔ ( Fun ◡ 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )
12	1 11	bitri	⊢ ( ◡ ◡ 𝐴 : dom 𝐴 –1-1→ V ↔ ( Fun ◡ 𝐴 ∧ Fun ◡ ◡ 𝐴 ) )