Metamath Proof Explorer
Description: An equality theorem for substitution. (Contributed by NM, 6Oct2004)
(Proof shortened by Andrew Salmon, 21Jun2011)


Ref 
Expression 

Assertion 
sbequ12r 
⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) 
Proof
Step 
Hyp 
Ref 
Expression 
1 

sbequ12 
⊢ ( 𝑦 = 𝑥 → ( 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) ) 
2 
1

bicomd 
⊢ ( 𝑦 = 𝑥 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) 
3 
2

equcoms 
⊢ ( 𝑥 = 𝑦 → ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) 