Theorem hbsb 1331

Description: If z is not free in φ, it is not free in [y / x]φ when y and z are distinct.

Hypothesis

Ref	Expression
hbsb.1	⊢ (φ → ∀zφ)

Assertion

Ref	Expression
hbsb	⊢ ([y / x]φ → ∀z[y / x]φ)

Distinct variable group:   y,z

Proof of Theorem hbsb

Step	Hyp	Ref	Expression
1		ax-16 1208	. 2 ⊢ (∀z z = y → ([y / x]φ → ∀z[y / x]φ))
2		hbsb.1	. . 3 ⊢ (φ → ∀zφ)
3	2	hbsb4 1246	. 2 ⊢ (¬ ∀z z = y → ([y / x]φ → ∀z[y / x]φ))
4	1, 3	pm2.61i 126	1 ⊢ ([y / x]φ → ∀z[y / x]φ)

Syntax hints:   → wi 3  ∀wal 952  [wsbc 1168

This theorem is referenced by:  2sb5rf 1336  2sb6rf 1337  sb10f 1340  2mo 1445  2eu6 1452  hbsbcg 1947  opabsb 2810  isarep1 3569  oprabval4g 4022

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain