Theorem rabbidv 3051

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 463	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	rabbidva 3050	1 |- ( ph -> { x e. A | ps } = { x e. A | ch } )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1405   e. wcel 1842   {crab 2758

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-ral 2759  df-rab 2763

This theorem is referenced by:  rabeqbidv  3054  difeq2  3555  seex  4786  mptiniseg  5317  dfpred3g  5378  elovmpt2rab  6502  elovmpt3rab1  6517  fineqvlem  7769  mapfien2  7902  supeq1  7938  supeq2  7941  supeq3  7942  oieq1  7971  oieq2  7972  ordtypecbv  7976  ordtypelem3  7979  harval  8022  inf3lema  8074  wemapwe  8171  wemapweOLD  8172  oef1o  8173  oef1oOLD  8174  tz9.12lem3  8239  rankvalb  8247  rankvalg  8267  ranksnb  8277  rankonidlem  8278  cardval3  8365  cardidm  8372  alephsuc2  8493  coftr  8685  fin1a2lem11  8822  fin1a2lem12  8823  hsmex  8844  axdc3lem2  8863  zorn2lem1  8908  zorn2lem6  8913  zorn2lem7  8914  zorn2g  8915  wuncval  9150  tskmval  9247  peano5uzti  10993  uzval  11129  reexALT  11259  ixxval  11590  fzval  11728  hashbclem  12550  hashbc  12551  shftfn  13055  rpnnen  14169  bitsfval  14282  sadfval  14311  sadcom  14322  smufval  14336  smupp1  14339  smupval  14347  smumullem  14351  gcdval  14355  bezoutlem2  14386  bezoutlem4  14388  isprm  14428  isprm2lem  14433  odzval  14527  pcval  14577  pceulem  14578  pceu  14579  pczpre  14580  pcdiv  14585  prmreclem1  14643  prmreclem4  14646  prmreclem5  14647  ramval  14735  cshws0  14795  imasdsval  15129  mrcval  15224  eldmcoa  15668  cycsubg2  16562  cntzval  16683  cntzsnval  16686  odfval  16881  odval  16882  gexval  16922  efgsfo  17081  dprdval  17354  dprdvalOLD  17356  ablfac1a  17440  ablfac1b  17441  ablfac1eu  17444  ablfaclem1  17456  ablfaclem3  17458  lspval  17941  aspval  18297  psrass1lem  18349  psrmulval  18359  mplmonmul  18446  coe1mul2  18630  ocvval  18996  dsmmelbas  19068  frlmsslss  19100  pmatcoe1fsupp  19494  istopon  19718  clsval  19830  neival  19896  ordtbaslem  19982  ordtbas2  19985  ordtopn1  19988  ordtopn2  19989  cnpval  20030  llyeq  20263  nllyeq  20264  ptfinfin  20312  finlocfin  20313  dissnlocfin  20322  locfindis  20323  xkoopn  20382  kqfval  20516  tsmsfbas  20918  blvalps  21180  blval  21181  nmofval  21513  nmoval  21514  ishtpy  21764  minveclem3b  22135  minveclem3  22136  minveclem4  22139  minveclem5  22140  ovolval  22177  vitalilem2  22310  vitalilem3  22311  vitalilem4  22312  vitali  22314  itg2monolem1  22449  elcpn  22629  mdegmullem  22770  elqaalem1  23007  elqaalem2  23008  elqaalem3  23009  elqaa  23010  aannenlem1  23016  aannenlem2  23017  jensen  23644  vmaval  23768  muval  23787  sgmval  23797  fsumdvdscom  23842  musum  23848  muinv  23850  dchrisum0fval  24071  dchrisum0ff  24073  logsqvma2  24109  pntrlog2bndlem1  24143  tglngval  24321  ttgval  24595  ttgitvval  24602  ebtwntg  24702  nbgraopALT  24841  nbgraop1  24842  wwlkn  25099  clwwlkn  25184  hashecclwwlkn1  25251  usghashecclwwlk  25252  2wlkonot  25282  2spthonot  25283  2pthwlkonot  25302  vdgrval  25313  rusgraprop4  25361  rusgrasn  25362  rusgranumwwlkl1  25363  rusgranumwlklem1  25366  rusgranumwlklem3  25368  rusgranumwlks  25373  rusgranumwlkg  25375  eupath2  25397  usg2spot2nb  25482  usgreg2spot  25484  2spotmdisj  25485  usgreghash2spot  25486  numclwwlkdisj  25497  numclwwlk3lem  25525  numclwwlk5  25529  sspval  26050  ubthlem1  26200  ubthlem2  26201  ubthlem3  26202  ocval  26612  spanval  26665  chsupid  26744  eigvecval  27228  specval  27230  iunpreima  27862  aciunf1  27947  crefeq  28301  ordtcnvNEW  28355  ordtrest2NEW  28358  ordtconlem1  28359  measvuni  28662  brfae  28697  omsfval  28742  orvcelval  28913  ballotlemi  28945  bnj602  29300  subfacp1lem6  29482  kur14  29513  cvmscbv  29555  cvmsi  29562  cvmsval  29563  snmlval  29628  snmlflim  29629  fvray  30479  fwddifnval  30501  neibastop3  30590  icoreval  31270  fin2so  31412  ftc1anclem6  31468  islinei  32757  pmapval  32774  paddval  32815  paddcom  32830  pclvalN  32907  ldilset  33126  dilsetN  33171  diafval  34051  diaval  34052  docavalN  34143  dicfval  34195  dochfval  34370  dochval  34371  mapdval  34648  mapdsn2  34662  2rexfrabdioph  35091  3rexfrabdioph  35092  4rexfrabdioph  35093  6rexfrabdioph  35094  7rexfrabdioph  35095  eldioph4i  35107  diophren  35108  pell1qrval  35143  pell14qrval  35145  pell1234qrval  35147  rpnnen3  35336  fnwe2lem1  35358  pwssplit4  35397  pwslnmlem2  35401  mapfien2OLD  35404  dgraaval  35457  itgoval  35474  rgspnval  35481  proot1hash  35524  lcmval  36046  nzss  36070  dvnprodlem1  37111  dvnprodlem2  37112  dvnprodlem3  37113  dvnprod  37114  stoweidlem26  37176  stoweidlem27  37177  stoweidlem31  37181  stoweidlem34  37184  stoweidlem46  37196  fourierdlem79  37336  fourierdlem96  37353  fourierdlem97  37354  fourierdlem98  37355  fourierdlem99  37356  fourierdlem105  37362  fourierdlem107  37364  fourierdlem108  37365  fourierdlem110  37367  etransclem11  37396  rnghmval  38208  bigoval  38680