Theorem hbopab1 2813

Description: The first abstraction variable in an ordered-pair class abstraction (class builder) is effectively not free.

Assertion

Ref	Expression
hbopab1	|- (z e. {<.x, y>. | ph} -> A.x z e. {<.x, y>. | ph})

Distinct variable group:   x,z

Proof of Theorem hbopab1

Step	Hyp	Ref	Expression
1		df-opab 2667	. 2 |- {<.x, y>. | ph} = {w | E.xE.y(w = <.x, y>. /\ ph)}
2		hbe1 1016	. . 3 |- (E.xE.y(w = <.x, y>. /\ ph) -> A.xE.xE.y(w = <.x, y>. /\ ph))
3	2	hbab 1467	. 2 |- (z e. {w | E.xE.y(w = <.x, y>. /\ ph)} -> A.x z e. {w | E.xE.y(w = <.x, y>. /\ ph)})
4	1, 3	hbxfr 1563	1 |- (z e. {<.x, y>. | ph} -> A.x z e. {<.x, y>. | ph})

Syntax hints:   -> wi 3   /\ wa 223  A.wal 954   = wceq 956   e. wcel 958  E.wex 980  {cab 1463  <.cop 2411  {copab 2666

This theorem is referenced by:  opabsb 2815  ssopab2 2822  dmopab 3320  rnopab 3353  cnvopab 3445  funopab 3548  zfrep6 3614  fnopabg 3615  fvopab5 3793  elrnopabg 3800  fopab2 3823  rnssopab 3825  fopabco 3832  fopabsn 3840  abrexexlem2 3859  rdgsucopab 3946  rdgsucopabn 3947  frsucopab 3954  abianfplem 3961  dom2d 4404  pw2en 4446  mapxpen 4495  xpmapenlem1 4496  xpmapenlem4 4499  unbnn 4544  inf0 4606  trcl 4645  ac6lem 4754  iundom 4812  alephfplem2 4897  om2uzsuc 6296  hbsum1 6983  fsumserz2 7003  serzfsum 7004  fsum1 7005  fsump1 7006  isumval2t 7194  isumclim3t 7200  isumclim4t 7201  isumcmpi 7215  geoisum1c 7245  cnlnadjlem5 10004  hbcmpt 10462

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-8 964  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-opab 2667

Copyright terms: Public domain