Theorem rabbidv 3189

Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 10-Feb-1995.)

Hypothesis

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

Assertion

Ref	Expression
rabbidv	|- ( ph -> { x e. A | ps } = { x e. A | ch } )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rabbidv

Step	Hyp	Ref	Expression
1		rabbidv.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2	1	adantr 481	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rabbidva 3188	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   e. wcel 1990   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-rab 2921

This theorem is referenced by:  rabeqbidv  3195  difeq2  3722  seex  5077  mptiniseg  5629  dfpred3g  5691  elovmpt2rab  6880  elovmpt3rab1  6893  fineqvlem  8174  mapfien2  8314  supeq1  8351  supeq2  8354  supeq3  8355  oieq1  8417  oieq2  8418  ordtypecbv  8422  ordtypelem3  8425  harval  8467  inf3lema  8521  wemapwe  8594  oef1o  8595  tz9.12lem3  8652  rankvalb  8660  rankvalg  8680  ranksnb  8690  rankonidlem  8691  cardval3  8778  cardidm  8785  alephsuc2  8903  coftr  9095  fin1a2lem11  9232  fin1a2lem12  9233  hsmex  9254  axdc3lem2  9273  zorn2lem1  9318  zorn2lem6  9323  zorn2lem7  9324  zorn2g  9325  wuncval  9564  tskmval  9661  peano5uzti  11467  uzval  11689  rpnnen1  11820  ixxval  12183  fzval  12328  hashbclem  13236  hashbc  13237  shftfn  13813  bitsfval  15145  sadfval  15174  sadcom  15185  smufval  15199  smupp1  15202  smupval  15210  smumullem  15214  gcdval  15218  bezoutlem2  15257  bezoutlem4  15259  lcmval  15305  lcmfval  15334  lcmf0val  15335  lcmfpr  15340  isprm  15387  odzval  15496  pcval  15549  pceulem  15550  pceu  15551  pczpre  15552  pcdiv  15557  prmreclem1  15620  prmreclem4  15623  prmreclem5  15624  ramval  15712  cshws0  15808  imasdsval  16175  mrcval  16270  eldmcoa  16715  cycsubg2  17631  cntzval  17754  cntzsnval  17757  odfval  17952  odval  17953  gexval  17993  efgsfo  18152  dprdval  18402  ablfac1a  18468  ablfac1b  18469  ablfac1eu  18472  ablfaclem1  18484  ablfaclem3  18486  lspval  18975  aspval  19328  psrass1lem  19377  psrmulval  19386  mplmonmul  19464  coe1mul2  19639  ocvval  20011  dsmmelbas  20083  frlmsslss  20113  pmatcoe1fsupp  20506  istopon  20717  toponsspwpw  20726  clsval  20841  neival  20906  ordtbaslem  20992  ordtbas2  20995  ordtopn1  20998  ordtopn2  20999  cnpval  21040  llyeq  21273  nllyeq  21274  ptfinfin  21322  finlocfin  21323  dissnlocfin  21332  locfindis  21333  xkoopn  21392  kqfval  21526  tsmsfbas  21931  blvalps  22190  blval  22191  nmofval  22518  nmoval  22519  ishtpy  22771  minveclem3b  23199  minveclem3  23200  minveclem4  23203  minveclem5  23204  ovolval  23242  vitalilem2  23378  vitalilem3  23379  vitalilem4  23380  vitali  23382  itg2monolem1  23517  elcpn  23697  mdegmullem  23838  elqaalem1  24074  elqaalem2  24075  elqaalem3  24076  elqaa  24077  aannenlem1  24083  aannenlem2  24084  jensen  24715  vmaval  24839  muval  24858  sgmval  24868  fsumdvdscom  24911  musum  24917  muinv  24919  dchrisum0fval  25194  dchrisum0ff  25196  logsqvma2  25232  pntrlog2bndlem1  25266  tglngval  25446  ttgval  25755  ttgitvval  25762  ebtwntg  25862  numedglnl  26039  dfnbgr2  26235  dfnbgr3  26236  uvtxusgr  26303  vtxdgval  26364  rusgrnumwrdl2  26482  iswwlksnon  26740  wwlks2onv  26847  rusgrnumwwlks  26869  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwwlksndisj  26973  eupth2  27099  fusgreg2wsplem  27197  fusgreghash2wsp  27202  numclwwlk3lem  27241  sspval  27578  ubthlem1  27726  ubthlem2  27727  ubthlem3  27728  ocval  28139  spanval  28192  chsupid  28271  eigvecval  28755  specval  28757  iunpreima  29383  aciunf1  29463  crefeq  29912  ordtcnvNEW  29966  ordtrest2NEW  29969  ordtconnlem1  29970  measvuni  30277  brfae  30311  omsfval  30356  orvcelval  30530  ballotlemi  30562  bnj602  30985  subfacp1lem6  31167  kur14  31198  cvmscbv  31240  cvmsi  31247  cvmsval  31248  snmlval  31313  snmlflim  31314  scutval  31911  fvray  32248  fwddifnval  32270  neibastop3  32357  icoreval  33201  fin2so  33396  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  poimirlem32  33441  ftc1anclem6  33490  islinei  35026  pmapval  35043  paddval  35084  paddcom  35099  pclvalN  35176  ldilset  35395  dilsetN  35440  diafval  36320  diaval  36321  docavalN  36412  dicfval  36464  dochfval  36639  dochval  36640  mapdval  36917  mapdsn2  36931  2rexfrabdioph  37360  3rexfrabdioph  37361  4rexfrabdioph  37362  6rexfrabdioph  37363  7rexfrabdioph  37364  eldioph4i  37376  diophren  37377  pell1qrval  37410  pell14qrval  37412  pell1234qrval  37414  rpnnen3  37599  fnwe2lem1  37620  pwssplit4  37659  pwslnmlem2  37663  dgraaval  37714  itgoval  37731  rgspnval  37738  proot1hash  37778  rfovfvd  38296  rfovfvfvd  38297  rfovcnvf1od  38298  fsovrfovd  38303  fsovfvd  38304  fsovfvfvd  38305  fsovcnvlem  38307  nzss  38516  supminfxr  39694  dvnprodlem1  40161  dvnprodlem2  40162  dvnprodlem3  40163  dvnprod  40164  stoweidlem26  40243  stoweidlem27  40244  stoweidlem31  40248  stoweidlem34  40251  stoweidlem46  40263  fourierdlem79  40402  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem105  40428  fourierdlem107  40430  fourierdlem108  40431  fourierdlem110  40433  etransclem11  40462  salgenval  40541  subsaliuncl  40576  ovnval  40755  ovnval2  40759  ovnval2b  40766  ovncvrrp  40778  ovnsubaddlem1  40784  ovnsubadd  40786  ovncvr2  40825  hspmbl  40843  ovolval2  40858  ovnovollem3  40872  salpreimagelt  40918  salpreimalegt  40920  salpreimagtge  40934  salpreimaltle  40935  issmflem  40936  issmf  40937  salpreimagtlt  40939  smfpreimalt  40940  smfpreimaltf  40945  issmfle  40954  smfpimltxr  40956  smfpreimale  40963  issmfgt  40965  smfpreimagt  40970  issmfge  40978  smflimlem3  40981  smflimlem4  40982  smflim  40985  smfpimgtxr  40988  smfpreimage  40990  prmdvdsfmtnof1  41499  rnghmval  41891  bigoval  42343