Theorem sbhypf

Description: Introduce an explicit substitution into an implicit substitution hypothesis. See also csbhypf . (Contributed by Raph Levien, 10-Apr-2004)

	Ref	Expression
Hypotheses	sbhypf.1	⊢ Ⅎ 𝑥 𝜓
	sbhypf.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion	sbhypf	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		sbhypf.1	⊢ Ⅎ 𝑥 𝜓
2		sbhypf.2	⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 ) )
4	3	equsexvw	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 = 𝐴 ) ↔ 𝑦 = 𝐴 )
5		nfs1v	⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑
6	5 1	nfbi	⊢ Ⅎ 𝑥 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
7		sbequ12	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) )
8	7	bicomd	⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
9	8 2	sylan9bb	⊢ ( ( 𝑥 = 𝑦 ∧ 𝑥 = 𝐴 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
10	6 9	exlimi	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝑥 = 𝐴 ) → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
11	4 10	sylbir	⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )