Theorem wl-sbcom2d-lem2

Description: Lemma used to prove wl-sbcom2d . (Contributed by Wolf Lammen, 10-Aug-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	wl-sbcom2d-lem2	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ¬ ∀ 𝑦 𝑦 = 𝑥 )
2		naev	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ¬ ∀ 𝑦 𝑦 = 𝑣 )
3		naev	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ¬ ∀ 𝑦 𝑦 = 𝑢 )
4		naev	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ¬ ∀ 𝑥 𝑥 = 𝑢 )
5	1 2 3 4	wl-2sb6d	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) → 𝜑 ) ) )