Theorem hbal 700

Description: If x is not free in φ, it is not free in ∀yφ.

Hypothesis

Ref	Expression
hb.1	⊢ (φ → ∀xφ)

Assertion

Ref	Expression
hbal	⊢ (∀yφ → ∀x∀yφ)

Proof of Theorem hbal

Step	Hyp	Ref	Expression
1		hb.1	. . 3 ⊢ (φ → ∀xφ)
2	1	19.20i 691	. 2 ⊢ (∀yφ → ∀y∀xφ)
3		ax-7 676	. 2 ⊢ (∀y∀xφ → ∀x∀yφ)
4	2, 3	syl 12	1 ⊢ (∀yφ → ∀x∀yφ)

Syntax hints:   → wi 2  ∀wal 672

This theorem is referenced by:  hbex 701  aaan 794  sb8 918  cbval2 974  euf 1011  mo 1020  2eu3 1069  bm1.1 1088  hbeq 1171  hbral 1236  ralcom2 1314  axrep 1473  axrep2 1474  zfrep2 1475  hbint 1975  onminex 2275  dmcosseq 2572  axrepndlem1 3738  axacndlem4 3756  axacnd 3758  zfcndrep 3760  zfcndinf 3764  nnwof 4609

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-mp 6  ax-4 673  ax-5 674  ax-7 676  ax-gen 677

metamath.org