Description: Obsolete version of sb5 as of 21-Sep-2024. (Contributed by NM, 18-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | sb5OLD | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfs1v | ⊢ Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 | |
2 | sbequ12 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) ) | |
3 | 1 2 | equsexv | ⊢ ( ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ↔ [ 𝑦 / 𝑥 ] 𝜑 ) |
4 | 3 | bicomi | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) |