Theorem hbs1 1371

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 1247	. 2 |- (A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
2		hbsb2 1264	. 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 990  [wsbc 1207

This theorem is referenced by:  eu1 1431  mo 1432  mopick 1472  2mo 1487  2eu6 1494  hbab1 1508  clelab 1624  moi2 1970  moi 1971  reu2 1976  sbhypf 1985  sbralie 1986  hbsbc1g 1993  elrabsf 2011  cbvralsv 2015  cbvrexsv 2016  csbabg 2095  iunrab 2664  cbvopab1s 2749  opabid 2887  opelopabsb 2892  opelopabf 2899  tfis 3208  tfinds 3212  tfindes 3215  findes 3248  ralxpf 3303  isarep1 3683  abrexex2 3985  oprabval4g 4091  cau3ii 7117  abrexex2g 11825

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-10 1002  ax-12 1004  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209

Copyright terms: Public domain