Theorem hbs1 1334

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 1212	. 2 |- (A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
2		hbsb2 1229	. 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 956  [wsbc 1172

This theorem is referenced by:  eu1 1394  mo 1395  mopick 1435  2mo 1450  2eu6 1457  hbab1 1469  clelab 1584  moi2 1927  moi 1928  reu2 1933  sbhypf 1942  sbhyp 1943  sbralie 1944  hbsbc1g 1951  elrabsf 1966  cbvralsv 1970  cbvrexsv 1971  csbabg 2046  iunrab 2600  cbvopab1s 2680  moop2 2807  opabid 2816  opabsb 2821  tfis 3133  findes 3166  tfinds 3167  tfindes 3170  ralxpf 3226  isarep1 3583  fvopabgf 3793  fvopabnf 3794  abrexex2 3877  oprabval4g 4037  seq1lem1 6310  cau3i 6914

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-10 968  ax-12 970  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220

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

Copyright terms: Public domain