Theorem hbab 1460

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 1206	. . 3 |- (A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
2		hbab.1	. . . 4 |- (ph -> A.xph)
3	2	hbsb4 1243	. . 3 |- (-. A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
4	1, 3	pm2.61i 126	. 2 |- ([z / y]ph -> A.x[z / y]ph)
5		df-clab 1457	. 2 |- (z e. {y | ph} <-> [z / y]ph)
6	5	albii 996	. 2 |- (A.x z e. {y | ph} <-> A.x[z / y]ph)
7	4, 5, 6	3imtr4 219	1 |- (z e. {y | ph} -> A.x z e. {y | ph})

Syntax hints:   -> wi 3  A.wal 951   = wceq 953   e. wcel 955  [wsbc 1166  {cab 1456

This theorem is referenced by:  hbrab 1765  cbvab 1899  hbeqd 1904  hbeld 1905  hbsbc1gd 1973  hbsbcgd 1974  hbif 2363  hbopd 2488  intab 2550  hbiu1 2574  hbii1 2575  hbbrd 2649  moop2 2790  hbopab1 2802  hbopab2 2803  hbimad 3396  hbfv 3714  hbfvd 3715  hbfvd2 3716  fvopabgf 3772  fvopabnf 3773  hbrdg 3921  hboprd 3967  hboprab1 3978  hboprab2 3979  oprabval4g 4016  hta 4700  hbnegd 5335  seq1lem1 6246  hbsum1 6921  hbsum 6922  fsum1f 6945  fsump1f 6949

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457

Copyright terms: Public domain