Theorem hbab 1467

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 1210	. . 3 |- (A.x x = z -> ([z / y]ph -> A.x[z / y]ph))
2		hbab.1	. . . 4 |- (ph -> A.xph)
3	2	hbsb4 1248	. . 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 1464	. 2 |- (z e. {y | ph} <-> [z / y]ph)
6	5	albii 999	. 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 954   = wceq 956   e. wcel 958  [wsbc 1170  {cab 1463

This theorem is referenced by:  hbrab 1772  cbvab 1906  hbeqd 1911  hbeld 1912  hbsbc1gd 1981  hbsbcgd 1982  hbif 2371  hbopd 2495  intab 2558  hbiu1 2582  hbii1 2583  hbbrd 2657  moop2 2799  hbopab1 2811  hbopab2 2812  hbimad 3410  hbfv 3727  hbfvd 3728  hbfvd2 3729  fvopabgf 3785  fvopabnf 3786  hbrdg 3934  hboprd 3980  hboprab1 3991  hboprab2 3992  oprabval4g 4029  hta 4716  hbnegd 5351  seq1lem1 6273  hbsum1 6941  hbsum 6942  fsum1f 6965  fsump1f 6969

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464

Copyright terms: Public domain