Theorem hbs1 1314

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 1194	. 2 |- (A.x x = y -> ([y / x]ph -> A.x[y / x]ph))
2		hbsb2 1211	. 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 950  [wsbc 1153

This theorem is referenced by:  eu1 1369  mo 1370  mopick 1410  2mo 1424  2eu6 1431  hbab1 1443  clelab 1557  moi 1896  reu2 1901  sbhypf 1910  sbhyp 1911  sbralie 1912  hbsbc1g 1919  elrabsf 1934  cbvralsv 1938  cbvrexsv 1939  csbabg 2014  iunrab 2564  cbvopab1s 2643  moop2 2766  opabid 2772  opabsb 2777  tfis 3090  findes 3123  tfinds 3124  tfindes 3127  ralxpf 3182  isarep1 3517  fvopabgf 3726  fvopabnf 3727  abrexex2 3810  oprabval4g 3970  seq1lem1 6197  cau3i 6802

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-16 1194  ax-11o 1202

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155

Copyright terms: Public domain