Theorem opabbii 2661

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 1468	. 2 |- z = z
2		opabbii.1	. . . 4 |- (ph <-> ps)
3	2	a1i 8	. . 3 |- (z = z -> (ph <-> ps))
4	3	opabbidv 2660	. 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 146   = wceq 953  {copab 2656

This theorem is referenced by:  fconstopab 3200  xpundi 3215  xpundir 3216  cnvco 3289  resopab 3379  fvopabg 3770  fopabap 3826  abrexexlem2 3844  dfrdg2 3918  dmoprabss 3988  resoprab 3994  fnoprval 4002  oprabval6g 4017  fo1st 4075  fo2nd 4076  1st2val 4079  2nd2val 4080  dfoprab3 4098  dfoprab5 4099  foprab2 4103  fvopabf4 4324  genpdm 5077  sqrval 6601  serzfsum 6942  serzclim0 7046  geosum 7176  geoisum 7177  geoisum1 7179  efclt 7254  efcvgfsum 7257  erelem6 7266  efcj 7278  ntrfval 7609  clsfval 7610  ntrval 7618  clsval 7619  neifval 7655  neif 7656  neival 7658  lpfval 7683  lpval 7684  dfms2 7738  lmfval 7863  xplm 7909  oprcn 7911  opr1scn 7914  fsumcnlem 7923  bcthlem12 7944  ip1cnilem4 8310  ip1cnilem6 8312  nmofval 8357  ajfval 8400  ipasslem6 8426  h2hlm 8789  dfhnorm2 8909  hilnorm 8951  ocvalt 9069  dfchsup2 9213  spanvalt 9214  hsupval2t 9215  dfadj2 9729  cnvadj 9733  dmadjss 9736  bra0 9790  cdj3lem3 10270  cdj3lem3b 10272  dmhmph 10419  rnhmph 10420

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-opab 2657

Copyright terms: Public domain