Theorem dfsb2

Description: An alternate definition of proper substitution that, like dfsb1 , mixes free and bound variables to avoid distinct variable requirements. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 17-Feb-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	dfsb2	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sp	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2		sbequ2	⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) )
3	2	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 → 𝜑 ) )
4		orc	⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
5	1 3 4	syl6an	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
6		sb4b	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
7		olc	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
8	6 7	syl6bi	⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ) )
9	5 8	pm2.61i	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )
10		sbequ1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
11	10	imp	⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → [ 𝑦 / 𝑥 ] 𝜑 )
12		sb2	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) → [ 𝑦 / 𝑥 ] 𝜑 )
13	11 12	jaoi	⊢ ( ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) → [ 𝑦 / 𝑥 ] 𝜑 )
14	9 13	impbii	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) ∨ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) )