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	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		nf3	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) )
2		abv	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑥 𝜑 )
3		ab0	⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ ∀ 𝑥 ¬ 𝜑 )
4	2 3	orbi12i	⊢ ( ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ ) ↔ ( ∀ 𝑥 𝜑 ∨ ∀ 𝑥 ¬ 𝜑 ) )
5	1 4	bitr4i	⊢ ( Ⅎ 𝑥 𝜑 ↔ ( { 𝑥 ∣ 𝜑 } = V ∨ { 𝑥 ∣ 𝜑 } = ∅ ) )