Theorem opabbii 2745

Description: Equivalent wff's yield equal class abstractions.

Hypothesis

Ref	Expression
opabbii.1	|- (ph <-> ps)

Assertion

Ref	Expression
opabbii	|- {<.x, y>. | ph} = {<.x, y>. | ps}

Distinct variable group:   x,y

Proof of Theorem opabbii

Step	Hyp	Ref	Expression
1		eqid 1518	. 2 |- z = z
2		opabbii.1	. . . 4 |- (ph <-> ps)
3	2	a1i 8	. . 3 |- (z = z -> (ph <-> ps))
4	3	opabbidv 2744	. 2 |- (z = z -> {<.x, y>. | ph} = {<.x, y>. | ps})
5	1, 4	ax-mp 7	1 |- {<.x, y>. | ph} = {<.x, y>. | ps}

Syntax hints:   <-> wb 144   = wceq 992  {copab 2740

This theorem is referenced by:  fconstopab 3293  xpundi 3310  xpundir 3311  cnvco 3391  resopab 3485  fvopabg 3896  fopabap 3955  abrexexlem2 3973  dmoprabss 4063  resoprab 4069  fnoprv 4077  oprabval6g 4093  fo1st 4152  fo2nd 4153  1st2val 4158  2nd2val 4159  dfoprab3 4174  dfoprab3s 4175  dfoprab4s 4176  foprab2 4181  df1st2 4188  df2nd2 4189  fparlem1 4199  fparlem2 4200  dfrdg2 4234  fvopabf4 4481  genpdm 5259  sqrval 6872  serzfsum 7207  serzclim0 7312  geosumi 7446  geoisum 7447  geoisum1 7449  efcl 7517  efcvgfsum 7520  erelem6 7529  efcji 7541  ntrfval 7877  clsfval 7878  ntrval 7886  clsval 7887  neifval 7924  neif 7925  neival 7927  lpfval 7952  lpval 7953  dfms2 8009  lmfval 8136  xplm 8186  oprcn 8188  opr1scn 8191  fsumcnlem 8200  bcthlem12 8221  ip1cnilem4 8630  ip1cnilem6 8632  nmofval 8679  ajfval 8724  ipasslem6 8751  h2hlm 9125  dfhnorm2 9264  hilnormi 9306  ocval 9429  dfchsup2 9574  spanval 9575  hsupval2 9576  dfadj2 10092  cnvadj 10096  dmadjss 10099  bra0 10154  cdj3lem3 10647  cdj3lem3b 10649  domncnt 10872  ranncnt 10873  dmhmph 11038  rnhmph 11039  limfillem1 11101  fictblem 11422  fictb 11423  ordtype 11434  neibastop2lem3 11582  neibastop2lem4 11583  fclusff 11735  geomcau 11914  piececn 11955  phtpycom 12092  phtpycolem3 12095  phtpycolem4 12096  phtpcval 12100

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-opab 2741

Copyright terms: Public domain