Metamath Proof Explorer


Theorem hblem

Description: Change the free variable of a hypothesis builder. (Contributed by NM, 21-Jun-1993) (Revised by Andrew Salmon, 11-Jul-2011) Add disjoint variable condition to avoid ax-13 . See hblemg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

Ref Expression
Hypothesis hblem.1 ( 𝑦𝐴 → ∀ 𝑥 𝑦𝐴 )
Assertion hblem ( 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 )

Proof

Step Hyp Ref Expression
1 hblem.1 ( 𝑦𝐴 → ∀ 𝑥 𝑦𝐴 )
2 1 hbsbw ( [ 𝑧 / 𝑦 ] 𝑦𝐴 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝑦𝐴 )
3 clelsb3 ( [ 𝑧 / 𝑦 ] 𝑦𝐴𝑧𝐴 )
4 3 albii ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝑦𝐴 ↔ ∀ 𝑥 𝑧𝐴 )
5 2 3 4 3imtr3i ( 𝑧𝐴 → ∀ 𝑥 𝑧𝐴 )