Theorem wl-sbcom2d-lem1

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

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

Proof

Step	Hyp	Ref	Expression
1		nfna1	⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑤
2		nfeqf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑤 → Ⅎ 𝑥 𝑣 = 𝑤 )
3	1 2	nfan1	⊢ Ⅎ 𝑥 ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ 𝑣 = 𝑤 )
4		sbequ	⊢ ( 𝑣 = 𝑤 → ( [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑤 / 𝑧 ] 𝜑 ) )
5	4	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ 𝑣 = 𝑤 ) → ( [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑤 / 𝑧 ] 𝜑 ) )
6	3 5	sbbid	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑤 ∧ 𝑣 = 𝑤 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑢 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
7	6	ancoms	⊢ ( ( 𝑣 = 𝑤 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑢 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
8		sbequ	⊢ ( 𝑢 = 𝑦 → ( [ 𝑢 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
9	7 8	sylan9bbr	⊢ ( ( 𝑢 = 𝑦 ∧ ( 𝑣 = 𝑤 ∧ ¬ ∀ 𝑥 𝑥 = 𝑤 ) ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) )
10	9	expr	⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑤 ) → ( ¬ ∀ 𝑥 𝑥 = 𝑤 → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑧 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑧 ] 𝜑 ) ) )