Theorem hbs1 986

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(s):   x,y

Proof of Theorem hbs1

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

Syntax hints:   → wi 2  ∀wal 672   = weq 797  [wsb 852

This theorem is referenced by:  sb5 988  sb6 989  eu1 1019  mo 1020  mopick 1054  hbab1 1095  clelab 1187  reu2 1338  vsbcint 1438  sbralie 1439  hbsbcg 1445  elrabsf 1456  moop2 1910  iunrab 2022  opabid 2099  cbvopab1s 2107  opabsb 2114  tfis 2245  findes 2400  tfinds 2401  tfindes 2404  fvopabgf 2874  fvopabnf 2875  abrexex2 2915  oprabval4g 3053  seqlem1 4662

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org