Theorem nf2

Description: Alternate definition of non-freeness. (Contributed by BJ, 16-Sep-2021)

	Ref	Expression
Assertion	nf2	|- ( F/ x ph <-> ( A. x ph \/ -. E. x ph ) )

Proof

Step	Hyp	Ref	Expression
1		df-nf	|- ( F/ x ph <-> ( E. x ph -> A. x ph ) )
2		imor	|- ( ( E. x ph -> A. x ph ) <-> ( -. E. x ph \/ A. x ph ) )
3		orcom	|- ( ( -. E. x ph \/ A. x ph ) <-> ( A. x ph \/ -. E. x ph ) )
4	1 2 3	3bitri	|- ( F/ x ph <-> ( A. x ph \/ -. E. x ph ) )