This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )