Theorem hbsb3 1208

Description: If y is not free in φ, x is not free in [y / x]φ.

Hypothesis

Ref	Expression
hbsb3.1	⊢ (φ → ∀yφ)

Assertion

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

Proof of Theorem hbsb3

Step	Hyp	Ref	Expression
1		hbsb3.1	. . 3 ⊢ (φ → ∀yφ)
2	1	sbimi 1175	. 2 ⊢ ([y / x]φ → [y / x]∀yφ)
3		hbsb2a 1206	. 2 ⊢ ([y / x]∀yφ → ∀x[y / x]φ)
4	2, 3	syl 10	1 ⊢ ([y / x]φ → ∀x[y / x]φ)

Syntax hints:   → wi 3  ∀wal 956  [wsbc 1172

This theorem is referenced by:  ax16 1211  sbco2 1257  sb8 1263  ax16ALT 1273  mo 1395  axrepndlem1 4956  axrepndlem2 4957

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-11 969  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174

Copyright terms: Public domain