Theorem wl-sbal1

Description: A theorem used in elimination of disjoint variable restriction on x and y by replacing it with a distinctor -. A. x x = z . (Contributed by NM, 15-May-1993) Proof is based on wl-sbalnae now. See also sbal1 . (Revised by Wolf Lammen, 25-Jul-2019) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	wl-sbal1	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		naev	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ¬ ∀ 𝑥 𝑥 = 𝑦 )
2		wl-sbalnae	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑥 𝑥 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
3	1 2	mpancom	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )