Theorem hbab1 1466

Description: Bound-variable hypothesis builder for a class abstraction.

Assertion

Ref	Expression
hbab1	|- (y e. {x | ph} -> A.x y e. {x | ph})

Distinct variable group:   x,y

Proof of Theorem hbab1

Step	Hyp	Ref	Expression
1		hbs1 1332	. 2 |- ([y / x]ph -> A.x[y / x]ph)
2		df-clab 1464	. 2 |- (y e. {x | ph} <-> [y / x]ph)
3	2	albii 999	. 2 |- (A.x y e. {x | ph} <-> A.x[y / x]ph)
4	1, 2, 3	3imtr4 219	1 |- (y e. {x | ph} -> A.x y e. {x | ph})

Syntax hints:   -> wi 3  A.wal 954   e. wcel 958  [wsbc 1170  {cab 1463

This theorem is referenced by:  abeq2 1568  eq2ab 1573  hbrab1 1772  elabgt 1895  elabf 1896  elabgf 1898  cbvab 1908  ss2ab 2116  abn0 2290  eusn 2446  eluniab 2513  elintab 2544  ssintab 2550  zfrep4 2701  euuni 2881  reucl 2885  onminex 3020  iunon 3909  iinon 3910  iunfiOLD 4569  scott0 4717  scottexs 4718  scott0s 4719  cp 4722  hta 4728  cardprc 4861  tgval3t 7625

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-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