Theorem hbab 1465

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 1208	. . 3 |- (A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
2		hbab.1	. . . 4 |- (ph -> A.xph)
3	2	hbsb4 1246	. . 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 1462	. 2 |- (z e. {y | ph} <-> [z / y]ph)
6	5	albii 997	. 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 952   = wceq 954   e. wcel 956  [wsbc 1168  {cab 1461

This theorem is referenced by:  hbrab 1770  cbvab 1904  hbeqd 1909  hbeld 1910  hbsbc1gd 1979  hbsbcgd 1980  hbif 2369  hbopd 2493  intab 2555  hbiu1 2579  hbii1 2580  hbbrd 2654  moop2 2796  hbopab1 2808  hbopab2 2809  hbimad 3404  hbfv 3720  hbfvd 3721  hbfvd2 3722  fvopabgf 3778  fvopabnf 3779  hbrdg 3927  hboprd 3973  hboprab1 3984  hboprab2 3985  oprabval4g 4022  hta 4708  hbnegd 5343  seq1lem1 6254  hbsum1 6929  hbsum 6930  fsum1f 6953  fsump1f 6957

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462

Copyright terms: Public domain