Theorem hbab 1444

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 1194	. . 3 |- (A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
2		hbab.1	. . . 4 |- (ph -> A.xph)
3	2	hbsb4 1232	. . 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 1441	. 2 |- (z e. {y | ph} <-> [z / y]ph)
6	5	albii 975	. 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 950   = wceq 1099   e. wcel 1105  [wsbc 1153  {cab 1440

This theorem is referenced by:  hbrab 1749  cbvab 1880  hbeqd 1885  hbeld 1886  hbsbc1gd 1954  hbsbcgd 1955  hbif 2344  hbopd 2466  intab 2528  hbiu1 2552  hbii1 2553  hbbrd 2627  moop2 2766  hbopab1 2775  hbopab2 2776  hbimad 3363  hbfv 3668  hbfvd 3669  hbfvd2 3670  fvopabgf 3726  fvopabnf 3727  hbrdg 3875  hboprd 3921  hboprab1 3932  hboprab2 3933  oprabval4g 3970  hta 4652  hbnegd 5286  seq1lem1 6197  hbsum1 6872  hbsum 6873  fsum1f 6896  fsump1f 6900

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  df-clab 1441

Copyright terms: Public domain