Theorem oprabbii 4923

Description: Equivalent wff's yield equal operation class abstractions.

Hypothesis

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

Assertion

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

Distinct variable group:   x,y,z

Proof of Theorem oprabbii

Step	Hyp	Ref	Expression
1		eqid 1884	. 2 |- w = w
2		oprabbii.1	. . . 4 |- (ph <-> ps)
3	2	a1i 8	. . 3 |- (w = w -> (ph <-> ps))
4	3	oprabbidv 4922	. 2 |- (w = w -> {<.<.x, y>., z>. | ph} = {<.<.x, y>., z>. | ps})
5	1, 4	ax-mp 7	1 |- {<.<.x, y>., z>. | ph} = {<.<.x, y>., z>. | ps}

Syntax hints:   <-> wb 163   = wceq 1298  {copab2 4885

This theorem is referenced by:  oprabval5 4958  oprec 5377  fnmap 5388  mapvalg 5389  pmvalg 5390  cdaval 6067  addcnsr 6405  mulcnsr 6406  dfioo2 7572  dfseq0 7806  cncfval 8526  blfval2 9113  blf 9121  cnnvm 9645  spwval2 9996  oprab2co 10160  symgoprab 10201  subsp 10244  filmapf 10307  flimff 10317  sshjval 10953  dfchj2 10957  dfchj3 10958  sshjval3 10959  hosmval 11144  hommval 11145  hodmval 11146  hfsmval 11147  hfmmval 11148  twsvbdop 14332  iscst1 14519  iscst2 14520  hmeogrp 14892  topgrpsubcnlem 14981  dualcat2lem 15129  dualded2lem 15130  dualded 15132  dualcat2 15133  ishoma 15136  isseg1 15304  isseg2 15305  fclusff 15623  eroprlem 15732  txcnoprab 15911  cnoproprabco 15919  cnoprab1 15921  cnoprab2 15922  phtpyfval 16046  phtpyval 16047  phtpycom 16050  phtpycolem3 16053  phtpycolem4 16054  reparphtlem2 16064  pcohtpylem3 16082  pcorevlem 16086  pi1fval 16092  pi1f 16093  pi1val 16094

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-opab 3396  df-oprab 4887

Copyright terms: Public domain