sbal1

Description: Check out sbal for a version not dependent on ax-13 . A theorem used in elimination of disjoint variable restriction on x and z by replacing it with a distinctor -. A. x x = z . (Contributed by NM, 15-May-1993) (Proof shortened by Wolf Lammen, 3-Oct-2018) (New usage is discouraged.) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		sb4b	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
2		nfnae	⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑧
3		nfeqf2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → Ⅎ 𝑥 𝑦 = 𝑧 )
4		19.21t	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ↔ ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) )
5	4	bicomd	⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → ( ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) )
6	3 5	syl	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) )
7	2 6	albid	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) )
8	1 7	sylan9bbr	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) )
9		nfnae	⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧
10		sb4b	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜑 ) ) )
11	9 10	albid	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜑 ) ) )
12		alcom	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) )
13	11 12	bitrdi	⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) )
14	13	adantl	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) )
15	8 14	bitr4d	⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑧 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
16	15	ex	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) ) )
17		sbequ12	⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) )
18	17	sps	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) )
19		sbequ12	⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )
20	19	sps	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )
21	20	dral2	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
22	18 21	bitr3d	⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )
23	16 22	pm2.61d2	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) )

Metamath Proof Explorer

Theorem sbal1

Proof