Theorem hbs1 1722

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

Syntax hints:   -> wi 3  A.wal 1296  [wsbc 1534

This theorem is referenced by:  eu1 1786  mo 1787  mopick 1833  2mo 1851  2eu6 1858  hbab1 1874  clelab 2013  cbvralf 2276  cbvrexf 2277  cbvrab 2421  moi2 2435  moi 2436  reu2 2442  sbhypf 2452  sbralie 2453  hbsbc1g 2461  elrabsf 2486  cbvralsv 2490  cbvralsvOLD 2491  cbvrexsv 2492  cbvrexsvOLD 2493  sbcralg 2531  sbcrexg 2533  sbcel12g 2552  sbceqdig 2554  csbabgOLD 2589  iunrab 3299  iinab 3317  cbvopab1 3405  cbvopab1s 3406  opabidOLD 3558  opelopabsbOLD 3565  opelopabf 3572  tfis 3938  tfinds 3942  tfindsOLD 3943  tfindes 3946  findes 3983  ralxpf 4043  isarep1 4497  isarep1OLD 4498  abrexex2 4847  oprabval4g 4960  cbvmpt 5011  cau3ii 8166  bnj34 12403  bnj37 12407  bnj37OLD 12408  bnj47 12417  bnj48 12422  bnj54OLD 12429  bnj58 12431  bnj971 12860  bnj1216 12989  bnj1306 13049  bnj1310 13050  bnj1366 13091  bnj1468 13145  bnj1492 13161  bnj607 13304  bnj873 13317  bnj849 13318  bnj1390 13513  setinds 13844  dfon2lem1 13849  tfisg 13912  wfisg 13917  frinsg 13941  abrexex2g 15738  pm14.24 16397  cbvralcsf 16411  cbvrexcsf 16412  cbvreucsf 16413  cbvrabcsf 16414  cbviotaf 16432

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-10 1308  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536

Copyright terms: Public domain