Theorem hbab 1503

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 1243	. . 3 |- (A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
2		hbab.1	. . . 4 |- (ph -> A.xph)
3	2	hbsb4 1281	. . 3 |- (-. A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
4	1, 3	pm2.61i 124	. 2 |- ([z / y]ph -> A.x[z / y]ph)
5		df-clab 1500	. 2 |- (z e. {y | ph} <-> [z / y]ph)
6	5	albii 1031	. 2 |- (A.x z e. {y | ph} <-> A.x[z / y]ph)
7	4, 5, 6	3imtr4i 217	1 |- (z e. {y | ph} -> A.x z e. {y | ph})

Syntax hints:   -> wi 3  A.wal 986   = wceq 988   e. wcel 990  [wsbc 1203  {cab 1499

This theorem is referenced by:  hbrab 1811  cbvab 1946  hbeqd 1951  hbeld 1952  hbsbc1gd 2023  hbsbcgd 2024  hbif 2418  hbopd 2545  intab 2608  hbiu1 2633  hbii1 2634  hbbrd 2709  hbopab1 2866  hbopab2 2867  hbimad 3475  hbfv 3805  hbfvd 3806  hbfvd2 3807  hbrdg 4012  hboprd 4058  hboprab1 4069  hboprab2 4070  oprabval4g 4108  hta 4814  hbnegd 5452  hbsum1 7106  hbsum 7107

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 994  ax-gen 995  ax-8 996  ax-10 998  ax-12 1000  ax-4 1005  ax-5o 1007  ax-6o 1010  ax-9o 1155  ax-10o 1173  ax-16 1243  ax-11o 1251

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1013  df-sb 1205  df-clab 1500

Copyright terms: Public domain