Theorem hbal 1002

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 989	. 2 ⊢ (∀yφ → ∀y∀xφ)
3		ax-7 959	. 2 ⊢ (∀y∀xφ → ∀x∀yφ)
4	2, 3	syl 10	1 ⊢ (∀yφ → ∀x∀yφ)

Syntax hints:   → wi 3  ∀wal 951

This theorem is referenced by:  hbex 1003  hba2 1010  aaan 1115  sb8 1256  cbval2 1311  euf 1377  mo 1386  2mo 1440  2eu3 1444  bm1.1 1455  hbeq 1557  hbral 1678  ralcom2 1768  moi 1915  uniiunlem 2122  hbint 2533  axrep1 2684  axrep2 2685  axrep3 2686  axrep4 2687  onminex 3010  dmcosseq 3349  axrepndlem1 4916  zfcndrep 4938  zfcndinf 4942  nnwof 6391

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7  ax-7 959  ax-gen 960  ax-4 970  ax-5o 972

Copyright terms: Public domain