Theorem hbs1 1365

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 1243	. 2 |- (A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
2		hbsb2 1260	. 2 |- (-. A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
3	1, 2	pm2.61i 124	1 |- ([y / x]ph -> A.x[y / x]ph)

Syntax hints:   -> wi 3  A.wal 986  [wsbc 1203

This theorem is referenced by:  eu1 1425  mo 1426  mopick 1466  2mo 1481  2eu6 1488  hbab1 1502  clelab 1618  moi2 1962  moi 1963  reu2 1968  sbhypf 1977  sbralie 1978  hbsbc1g 1985  elrabsf 2003  cbvralsv 2007  cbvrexsv 2008  csbabg 2087  iunrab 2645  cbvopab1s 2726  opabid 2863  opelopabsb 2868  opelopabf 2875  tfis 3182  tfinds 3186  tfindes 3189  findes 3222  ralxpf 3277  isarep1 3652  abrexex2 3947  oprabval4g 4108  cau3ii 7037

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-10 998  ax-12 1000  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-sb 1205

Copyright terms: Public domain