Theorem sb5ALT

Description: Equivalence for substitution. Alternate proof of sb5 . This proof is sb5ALTVD automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sb5ALT	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		equsb1	⊢ [ 𝑦 / 𝑥 ] 𝑥 = 𝑦
2		sban	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝑦 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) )
3	2	simplbi2com	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ( [ 𝑦 / 𝑥 ] 𝑥 = 𝑦 → [ 𝑦 / 𝑥 ] ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
4	1 3	mpi	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → [ 𝑦 / 𝑥 ] ( 𝑥 = 𝑦 ∧ 𝜑 ) )
5		spsbe	⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 = 𝑦 ∧ 𝜑 ) → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
6	4 5	syl	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
7		hbs1	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 )
8		simpr	⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → 𝜑 )
9	8	a1i	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → 𝜑 ) )
10		simpl	⊢ ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → 𝑥 = 𝑦 )
11	10	a1i	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → 𝑥 = 𝑦 ) )
12		sbequ1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 ) )
13	12	com12	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → [ 𝑦 / 𝑥 ] 𝜑 ) )
14	9 11 13	syl6c	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → ( ( 𝑥 = 𝑦 ∧ 𝜑 ) → [ 𝑦 / 𝑥 ] 𝜑 ) )
15	7 14	exlimexi	⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) → [ 𝑦 / 𝑥 ] 𝜑 )
16	6 15	impbii	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )