Theorem hbs1 1330

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

Assertion

Ref	Expression
hbs1	|- ([y / x]ph -> A.x[y / x]ph)

Distinct variable group:   x,y

Proof of Theorem hbs1

Step	Hyp	Ref	Expression
1		ax-16 1208	. 2 |- (A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
2		hbsb2 1225	. 2 |- (-. A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
3	1, 2	pm2.61i 126	1 |- ([y / x]ph -> A.x[y / x]ph)

Syntax hints:   -> wi 3  A.wal 952  [wsbc 1168

This theorem is referenced by:  eu1 1390  mo 1391  mopick 1431  2mo 1445  2eu6 1452  hbab1 1464  clelab 1578  moi2 1920  moi 1921  reu2 1926  sbhypf 1935  sbhyp 1936  sbralie 1937  hbsbc1g 1944  elrabsf 1959  cbvralsv 1963  cbvrexsv 1964  csbabg 2039  iunrab 2591  cbvopab1s 2670  moop2 2796  opabid 2805  opabsb 2810  tfis 3122  findes 3155  tfinds 3156  tfindes 3159  ralxpf 3215  isarep1 3569  fvopabgf 3778  fvopabnf 3779  abrexex2 3862  oprabval4g 4022  seq1lem1 6254  cau3i 6859

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-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