Theorem rabbidv 3101

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

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1395   e. wcel 1819   {crab 2811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-ral 2812  df-rab 2816

This theorem is referenced by:  rabeqbidv  3104  difeq2  3612  seex  4851  mptiniseg  5507  elovmpt2rab  6520  elovmpt3rab1  6535  fineqvlem  7753  mapfien2  7886  supeq1  7922  supeq2  7925  supeq3  7926  oieq1  7955  oieq2  7956  ordtypecbv  7960  ordtypelem3  7963  harval  8006  inf3lema  8058  wemapwe  8156  wemapweOLD  8157  oef1o  8158  oef1oOLD  8159  tz9.12lem3  8224  rankvalb  8232  rankvalg  8252  ranksnb  8262  rankonidlem  8263  cardval3  8350  cardidm  8357  alephsuc2  8478  coftr  8670  fin1a2lem11  8807  fin1a2lem12  8808  hsmex  8829  axdc3lem2  8848  zorn2lem1  8893  zorn2lem6  8898  zorn2lem7  8899  zorn2g  8900  wuncval  9137  tskmval  9234  peano5uzti  10973  uzval  11108  reexALT  11239  ixxval  11562  fzval  11699  hashbclem  12504  hashbc  12505  shftfn  12917  rpnnen  13971  bitsfval  14084  sadfval  14113  sadcom  14124  smufval  14138  smupp1  14141  smupval  14149  smumullem  14153  gcdval  14157  bezoutlem2  14188  bezoutlem4  14190  isprm  14230  isprm2lem  14235  odzval  14329  pcval  14379  pceulem  14380  pceu  14381  pczpre  14382  pcdiv  14387  prmreclem1  14445  prmreclem4  14448  prmreclem5  14449  ramval  14537  cshws0  14597  imasdsval  14931  mrcval  15026  eldmcoa  15470  cycsubg2  16364  cntzval  16485  cntzsnval  16488  odfval  16683  odval  16684  gexval  16724  efgsfo  16883  dprdval  17160  dprdvalOLD  17162  ablfac1a  17246  ablfac1b  17247  ablfac1eu  17250  ablfaclem1  17262  ablfaclem3  17264  lspval  17747  aspval  18103  psrass1lem  18155  psrmulval  18165  mplmonmul  18252  coe1mul2  18436  ocvval  18824  dsmmelbas  18896  frlmsslss  18930  pmatcoe1fsupp  19328  istopon  19552  clsval  19664  neival  19729  ordtbaslem  19815  ordtbas2  19818  ordtopn1  19821  ordtopn2  19822  cnpval  19863  llyeq  20096  nllyeq  20097  ptfinfin  20145  finlocfin  20146  dissnlocfin  20155  locfindis  20156  xkoopn  20215  kqfval  20349  tsmsfbas  20751  blvalps  21013  blval  21014  nmofval  21346  nmoval  21347  ishtpy  21597  minveclem3b  21968  minveclem3  21969  minveclem4  21972  minveclem5  21973  ovolval  22010  vitalilem2  22143  vitalilem3  22144  vitalilem4  22145  vitali  22147  itg2monolem1  22282  elcpn  22462  mdegmullem  22603  elqaalem1  22840  elqaalem2  22841  elqaalem3  22842  elqaa  22843  aannenlem1  22849  aannenlem2  22850  jensen  23443  vmaval  23512  muval  23531  sgmval  23541  fsumdvdscom  23586  musum  23592  muinv  23594  dchrisum0fval  23815  dchrisum0ff  23817  logsqvma2  23853  pntrlog2bndlem1  23887  tglngval  24063  ttgval  24304  ttgitvval  24311  ebtwntg  24411  nbgraopALT  24550  nbgraop1  24551  wwlkn  24808  clwwlkn  24893  hashecclwwlkn1  24960  usghashecclwwlk  24961  2wlkonot  24991  2spthonot  24992  2pthwlkonot  25011  vdgrval  25022  rusgraprop4  25070  rusgrasn  25071  rusgranumwwlkl1  25072  rusgranumwlklem1  25075  rusgranumwlklem3  25077  rusgranumwlks  25082  rusgranumwlkg  25084  eupath2  25106  usg2spot2nb  25191  usgreg2spot  25193  2spotmdisj  25194  usgreghash2spot  25195  numclwwlkdisj  25206  numclwwlk3lem  25234  numclwwlk5  25238  sspval  25762  ubthlem1  25912  ubthlem2  25913  ubthlem3  25914  ocval  26324  spanval  26377  chsupid  26456  eigvecval  26941  specval  26943  iunpreima  27569  aciunf1  27651  crefeq  28001  ordtcnvNEW  28055  ordtrest2NEW  28058  ordtconlem1  28059  measvuni  28346  brfae  28381  omsfval  28426  orvcelval  28582  ballotlemi  28614  subfacp1lem6  28804  kur14  28835  cvmscbv  28878  cvmsi  28885  cvmsval  28886  snmlval  28951  snmlflim  28952  dfpred3g  29429  fvray  29953  fin2so  30202  ftc1anclem6  30257  neibastop3  30342  2rexfrabdioph  30891  3rexfrabdioph  30892  4rexfrabdioph  30893  6rexfrabdioph  30894  7rexfrabdioph  30895  eldioph4i  30908  diophren  30909  pell1qrval  30944  pell14qrval  30946  pell1234qrval  30948  rpnnen3  31136  fnwe2lem1  31158  pwssplit4  31197  pwslnmlem2  31201  mapfien2OLD  31204  dgraaval  31255  itgoval  31272  rgspnval  31279  proot1hash  31322  lcmval  31360  nzss  31384  dvnprodlem1  31904  dvnprodlem2  31905  dvnprodlem3  31906  dvnprod  31907  stoweidlem26  31969  stoweidlem27  31970  stoweidlem31  31974  stoweidlem34  31977  stoweidlem46  31989  fourierdlem79  32129  fourierdlem96  32146  fourierdlem97  32147  fourierdlem98  32148  fourierdlem99  32149  fourierdlem105  32155  fourierdlem107  32157  fourierdlem108  32158  fourierdlem110  32160  etransclem11  32189  rnghmval  32799  bnj602  34074  islinei  35565  pmapval  35582  paddval  35623  paddcom  35638  pclvalN  35715  ldilset  35934  dilsetN  35979  diafval  36859  diaval  36860  docavalN  36951  dicfval  37003  dochfval  37178  dochval  37179  mapdval  37456  mapdsn2  37470