Theorem hbab 2132

Description: Bound-variable hypothesis builder for a class abstraction.

Hypothesis

Ref	Expression
hbab.1	|- (ph -> A.xph)

Assertion

Ref	Expression
hbab	|- (z e. {y | ph} -> A.x z e. {y | ph})

Distinct variable group:   x,z

Proof of Theorem hbab

Step	Hyp	Ref	Expression
1		ax-16 1854	. . 3 |- (A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
2		hbab.1	. . . 4 |- (ph -> A.xph)
3	2	hbsb4 1895	. . 3 |- (-. A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
4	1, 3	pm2.61i 192	. 2 |- ([z / y]ph -> A.x[z / y]ph)
5		df-clab 2129	. 2 |- (z e. {y | ph} <-> [z / y]ph)
6	5	albii 1635	. 2 |- (A.x z e. {y | ph} <-> A.x[z / y]ph)
7	4, 5, 6	3imtr4i 328	1 |- (z e. {y | ph} -> A.x z e. {y | ph})

Syntax hints:   -> wi 3  A.wal 1584   = wceq 1586   e. wcel 1588  [wsbc 1814  {cab 2128

This theorem is referenced by:  hbrab 2503  hbeqd 2665  hbeqdOLD 2666  hbeld 2668  hbsbc1gd 2749  hbsbcgd 2750  hbif 3196  hbopd 3355  intab 3428  hbiu1 3457  hbii1 3458  hbopab 3722  hbopab1 3723  hbopab2 3724  eusvobj1 3980  hbimad 4392  hbfv 4771  hbfvd 4772  hbfvd2 4773  hboprab1 5014  hboprab2 5015  oprabval4g 5054  hbiota 5222  hbrdg 5308  hta 6097  hbsum1 8639  hbsum 8640  bnj898 13586  bnj1347 13851  bnj1441 13905  bnj900 14096  bnj1014 14145  bnj1123 14193  bnj1309 14258  bnj1307 14259  bnj1398 14286  bnj1444 14305  bnj1445 14306  bnj1446 14307  bnj1447 14308  bnj1467 14320  bnj1499 14332  bnj1518 14338  bnj1519 14339  dfon2lem3 14485  hbprod1 15398  hbprod 15399  intopcoaconb 15662  intopcoaconc 15663  neibastop1 16342  neibastop2lem1 16343  neibastop2lem3 16345  neibastop2lem4 16346  neibastop3 16348  sdclem2 16634  sdc 16635

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-10 1596  ax-12 1598  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864

This theorem depends on definitions:  df-bi 220  df-an 339  df-ex 1616  df-sb 1816  df-clab 2129

Copyright terms: Public domain