Theorem nvof1ob

Description: A class equal to its converse is a function on a class if and only if it is a bijection from that class onto itself (the reverse implication holds without the hypothesis, see f1ofn ). (Contributed by BJ, 8-Nov-2026) Can shorten nvof1o using biimpac .

	Ref	Expression
Assertion	nvof1ob	⊢ ( ◡ 𝐹 = 𝐹 → ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶1-1onto 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dff1o4	⊢ ( 𝐹 : 𝐴 ⟶1-1onto 𝐴 ↔ ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐴 ) )
2		fneq1	⊢ ( ◡ 𝐹 = 𝐹 → ( ◡ 𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴 ) )
3	2	anbi2d	⊢ ( ◡ 𝐹 = 𝐹 → ( ( 𝐹 Fn 𝐴 ∧ ◡ 𝐹 Fn 𝐴 ) ↔ ( 𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) ) )
4	1 3	bitrid	⊢ ( ◡ 𝐹 = 𝐹 → ( 𝐹 : 𝐴 ⟶1-1onto 𝐴 ↔ ( 𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) ) )
5		anidm	⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝐹 Fn 𝐴 ) ↔ 𝐹 Fn 𝐴 )
6	4 5	bitr2di	⊢ ( ◡ 𝐹 = 𝐹 → ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶1-1onto 𝐴 ) )