Theorem hbab1 1469

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 1334	. 2 |- ([y / x]ph -> A.x[y / x]ph)
2		df-clab 1467	. 2 |- (y e. {x | ph} <-> [y / x]ph)
3	2	albii 1001	. 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 956   e. wcel 960  [wsbc 1172  {cab 1466

This theorem is referenced by:  abeq2 1571  eq2ab 1576  hbrab1 1775  elabgt 1898  elabf 1899  elabgf 1901  cbvab 1911  ss2ab 2119  abn0 2294  eusn 2450  eluniab 2517  elintab 2548  ssintab 2554  zfrep4 2706  euuni 2887  reucl 2891  onminex 3026  iunon 3915  iinon 3916  scott0 4727  scottexs 4728  scott0s 4729  cp 4732  hta 4738  cardprc 4872  tgval3t 7624

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-10 968  ax-12 970  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467

Copyright terms: Public domain