Theorem hbab1 1443

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 1314	. 2 |- ([y / x]ph -> A.x[y / x]ph)
2		df-clab 1441	. 2 |- (y e. {x | ph} <-> [y / x]ph)
3	2	albii 975	. 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 950   e. wcel 1105  [wsbc 1153  {cab 1440

This theorem is referenced by:  abeq2 1544  eq2ab 1549  hbrab1 1748  elabgt 1867  elabf 1868  elabgf 1870  cbvab 1880  ss2ab 2087  abn0 2261  eusn 2416  eluniab 2481  elintab 2512  ssintab 2518  zfrep4 2669  euuni 2844  reucl 2848  onminex 2983  iunon 3848  iinon 3849  iunfi 4495  scott0 4641  scottexs 4642  scott0s 4643  cp 4646  hta 4652  cardprc 4784  tgval3t 7518

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