Theorem bj-nfeel2

Description: Nonfreeness in a membership statement. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-nfeel2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 ∈ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		nfv	⊢ Ⅎ 𝑥 𝑡 ∈ 𝑧
2		elequ1	⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) )
3	1 2	bj-dvelimv	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 ∈ 𝑧 )