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	|- ( `' F = F -> ( F Fn A <-> F : A -1-1-onto-> A ) )

Proof

Step	Hyp	Ref	Expression
1		dff1o4	|- ( F : A -1-1-onto-> A <-> ( F Fn A /\ `' F Fn A ) )
2		fneq1	|- ( `' F = F -> ( `' F Fn A <-> F Fn A ) )
3	2	anbi2d	|- ( `' F = F -> ( ( F Fn A /\ `' F Fn A ) <-> ( F Fn A /\ F Fn A ) ) )
4	1 3	bitrid	|- ( `' F = F -> ( F : A -1-1-onto-> A <-> ( F Fn A /\ F Fn A ) ) )
5		anidm	|- ( ( F Fn A /\ F Fn A ) <-> F Fn A )
6	4 5	bitr2di	|- ( `' F = F -> ( F Fn A <-> F : A -1-1-onto-> A ) )