Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
The universal class
sbhypf
Metamath Proof Explorer
Description: Introduce an explicit substitution into an implicit substitution
hypothesis. See also csbhypf . (Contributed by Raph Levien , 10-Apr-2004) (Proof shortened by Wolf Lammen , 25-Jan-2025)
Ref
Expression
Hypotheses
sbhypf.1
⊢ Ⅎ 𝑥 𝜓
sbhypf.2
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
Assertion
sbhypf
⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
Proof
Step
Hyp
Ref
Expression
1
sbhypf.1
⊢ Ⅎ 𝑥 𝜓
2
sbhypf.2
⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜓 ) )
3
2
sbimi
⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 → [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜓 ) )
4
eqsb1
⊢ ( [ 𝑦 / 𝑥 ] 𝑥 = 𝐴 ↔ 𝑦 = 𝐴 )
5
1
sbf
⊢ ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜓 )
6
5
sblbis
⊢ ( [ 𝑦 / 𝑥 ] ( 𝜑 ↔ 𝜓 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )
7
3 4 6
3imtr3i
⊢ ( 𝑦 = 𝐴 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 ) )