Theorem hbs1 1331

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

Assertion

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

Distinct variable group:   x,y

Proof of Theorem hbs1

Step	Hyp	Ref	Expression
1		ax-16 1209	. 2 ⊢ (∀x x = y → ([y / x]φ → ∀x[y / x]φ))
2		hbsb2 1226	. 2 ⊢ (¬ ∀x x = y → ([y / x]φ → ∀x[y / x]φ))
3	1, 2	pm2.61i 126	1 ⊢ ([y / x]φ → ∀x[y / x]φ)

Syntax hints:   → wi 3  ∀wal 953  [wsbc 1169

This theorem is referenced by:  eu1 1391  mo 1392  mopick 1432  2mo 1446  2eu6 1453  hbab1 1465  clelab 1579  moi2 1921  moi 1922  reu2 1927  sbhypf 1936  sbhyp 1937  sbralie 1938  hbsbc1g 1945  elrabsf 1960  cbvralsv 1964  cbvrexsv 1965  csbabg 2040  iunrab 2592  cbvopab1s 2671  moop2 2797  opabid 2806  opabsb 2811  tfis 3123  findes 3156  tfinds 3157  tfindes 3160  ralxpf 3216  isarep1 3573  fvopabgf 3782  fvopabnf 3783  abrexex2 3866  oprabval4g 4026  seq1lem1 6259  cau3i 6866

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-10 965  ax-12 967  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171

Copyright terms: Public domain