Theorem hbrab1 1772

Description: The abstraction variable in a restricted class abstraction isn't free.

Assertion

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

Distinct variable group:   x,y

Proof of Theorem hbrab1

Step	Hyp	Ref	Expression
1		df-rab 1652	. 2 |- {x e. A | ph} = {x | (x e. A /\ ph)}
2		hbab1 1466	. 2 |- (y e. {x | (x e. A /\ ph)} -> A.x y e. {x | (x e. A /\ ph)})
3	1, 2	hbxfr 1563	1 |- (y e. {x e. A | ph} -> A.x y e. {x e. A | ph})

Syntax hints:   -> wi 3   /\ wa 223  A.wal 954   e. wcel 958  {cab 1463  {crab 1648

This theorem is referenced by:  reuuni2f 2883  reuuni4 2887  reuuniss 2889  reuuniss2 2891  reusn 2892  rabxfr 2902  reuunixfr 2906  onminsb 3009  oawordeulem 4188  tz9.12lem3 4661  rankid 4672  ondomcard 4857  cardmin 4860  alephordlem1 4872  cardaleph 4885  reuunineg 6066  nnwos 6460  minvecdist 8585  fgsb 10570  fgsbOLD 10571  fgsb2 10580

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-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-rab 1652

Copyright terms: Public domain