Theorem hbopab2 2809

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 2662	. 2 |- {<.x, y>. | ph} = {w | E.xE.y(w = <.x, y>. /\ ph)}
2		hbe1 1014	. . . 4 |- (E.y(w = <.x, y>. /\ ph) -> A.yE.y(w = <.x, y>. /\ ph))
3	2	hbex 1004	. . 3 |- (E.xE.y(w = <.x, y>. /\ ph) -> A.yE.xE.y(w = <.x, y>. /\ ph))
4	3	hbab 1465	. 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 1560	1 |- (z e. {<.x, y>. | ph} -> A.y z e. {<.x, y>. | ph})

Syntax hints:   -> wi 3   /\ wa 223  A.wal 952   = wceq 954   e. wcel 956  E.wex 978  {cab 1461  <.cop 2407  {copab 2661

This theorem is referenced by:  opabsb 2810  ssopab2 2817  dmopab 3315  rnopab 3347  cnvopab 3437  funopab 3540  zfrep6 3606  fnopabg 3607  fvopab2 3782  fvopab5 3784  fopab2 3814  abrexexlem2 3850  dom2d 4391  xpmapenlem1 4482  xpmapenlem4 4485

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-opab 2662

Copyright terms: Public domain