Theorem hbab1 1095

Description: The abstraction variable in an class abstraction is not free.

Assertion

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

Distinct variable group(s):   x,y

Proof of Theorem hbab1

Step	Hyp	Ref	Expression
1		hbs1 986	. 2 |- ([y / x]ph -> A.x[y / x]ph)
2		df-clab 1093	. 2 |- (y e. {x | ph} <-> [y / x]ph)
3	2	bial 695	. 2 |- (A.x y e. {x | ph} <-> A.x[y / x]ph)
4	1, 2, 3	3imtr4 192	1 |- (y e. {x | ph} -> A.x y e. {x | ph})

Syntax hints:   -> wi 2  A.wal 672  [wsb 852  {cab 1090   e. wcel 1092

This theorem is referenced by:  cleqab 1174  cleq2ab 1179  hbrab1 1310  elabf 1414  elabgf 1416  cbvab 1423  zfrep4 1479  ss2ab 1551  abn0 1715  eusn 1913  eluniab 1926  euuni 1954  reucl 1957  elintab 1976  onminex 2275  iunon 2947  iinon 2948  scott0 3542  scottexs 3543  scott0s 3544  cp 3547  hta 3619  cardprc 3667

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093

metamath.org