Theorem hblemg

Description: Change the free variable of a hypothesis builder. Usage of this theorem is discouraged because it depends on ax-13 . See hblem for a version with more disjoint variable conditions, but not requiring ax-13 . (Contributed by NM, 21-Jun-1993) (Revised by Andrew Salmon, 11-Jul-2011) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hblemg.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
Assertion	hblemg	⊢ ( 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hblemg.1	⊢ ( 𝑦 ∈ 𝐴 → ∀ 𝑥 𝑦 ∈ 𝐴 )
2	1	hbsb	⊢ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 → ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 )
3		clelsb1	⊢ ( [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴 )
4	3	albii	⊢ ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝑦 ∈ 𝐴 ↔ ∀ 𝑥 𝑧 ∈ 𝐴 )
5	2 3 4	3imtr3i	⊢ ( 𝑧 ∈ 𝐴 → ∀ 𝑥 𝑧 ∈ 𝐴 )