Theorem dfnf5

Description: Characterization of non-freeness in a formula in terms of its extension. (Contributed by BJ, 19-Mar-2021)

	Ref	Expression
Assertion	dfnf5	|- ( F/ x ph <-> ( { x | ph } = _V \/ { x | ph } = (/) ) )

Proof

Step	Hyp	Ref	Expression
1		nf3	|- ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )
2		abv	|- ( { x | ph } = _V <-> A. x ph )
3		ab0	|- ( { x | ph } = (/) <-> A. x -. ph )
4	2 3	orbi12i	|- ( ( { x | ph } = _V \/ { x | ph } = (/) ) <-> ( A. x ph \/ A. x -. ph ) )
5	1 4	bitr4i	|- ( F/ x ph <-> ( { x | ph } = _V \/ { x | ph } = (/) ) )