Theorem hbopab2 2814

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

Assertion

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

Distinct variable group:   y,z

Proof of Theorem hbopab2

Step	Hyp	Ref	Expression
1		df-opab 2667	. 2 |- {<.x, y>. | ph} = {w | E.xE.y(w = <.x, y>. /\ ph)}
2		hbe1 1016	. . . 4 |- (E.y(w = <.x, y>. /\ ph) -> A.yE.y(w = <.x, y>. /\ ph))
3	2	hbex 1006	. . 3 |- (E.xE.y(w = <.x, y>. /\ ph) -> A.yE.xE.y(w = <.x, y>. /\ ph))
4	3	hbab 1467	. 2 |- (z e. {w | E.xE.y(w = <.x, y>. /\ ph)} -> A.y z e. {w | E.xE.y(w = <.x, y>. /\ ph)})
5	1, 4	hbxfr 1563	1 |- (z e. {<.x, y>. | ph} -> A.y 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  fvopab2 3791  fvopab5 3793  fopab2 3823  abrexexlem2 3859  dom2d 4404  xpmapenlem1 4496  xpmapenlem4 4499

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