Theorem hbopab1 2808

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 2662	. 2 |- {<.x, y>. | ph} = {w | E.xE.y(w = <.x, y>. /\ ph)}
2		hbe1 1014	. . 3 |- (E.xE.y(w = <.x, y>. /\ ph) -> A.xE.xE.y(w = <.x, y>. /\ ph))
3	2	hbab 1465	. 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 1560	1 |- (z e. {<.x, y>. | ph} -> A.x 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  fvopab5 3784  elrnopabg 3791  fopab2 3814  rnssopab 3816  fopabco 3823  fopabsn 3831  abrexexlem2 3850  rdgsucopab 3937  rdgsucopabn 3938  frsucopab 3945  abianfplem 3952  dom2d 4391  pw2en 4432  mapxpen 4481  xpmapenlem1 4482  xpmapenlem4 4485  unbnn 4527  inf0 4586  trcl 4625  ac6lem 4734  iundom 4792  alephfplem2 4877  om2uzsuc 6241  hbsum1 6929  fsumserz2 6949  serzfsum 6950  fsum1 6951  fsump1 6952  isumval2t 7138  isumclim3t 7143  isumclim4t 7144  isumcmpi 7158  geoisum1c 7188  cnlnadjlem5 9942  hbcmpt 10394

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