Theorem rabbidv 3022

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

Syntax hints:   -> wi 4   <-> wb 189   = wceq 1452   e. wcel 1904   {crab 2760

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-ral 2761  df-rab 2765

This theorem is referenced by:  rabeqbidv  3026  difeq2  3534  seex  4802  mptiniseg  5336  dfpred3g  5398  elovmpt2rab  6534  elovmpt3rab1  6546  fineqvlem  7804  mapfien2  7940  supeq1  7977  supeq2  7980  supeq3  7981  oieq1  8045  oieq2  8046  ordtypecbv  8050  ordtypelem3  8053  harval  8095  inf3lema  8147  wemapwe  8220  oef1o  8221  tz9.12lem3  8278  rankvalb  8286  rankvalg  8306  ranksnb  8316  rankonidlem  8317  cardval3  8404  cardidm  8411  alephsuc2  8529  coftr  8721  fin1a2lem11  8858  fin1a2lem12  8859  hsmex  8880  axdc3lem2  8899  zorn2lem1  8944  zorn2lem6  8949  zorn2lem7  8950  zorn2g  8951  wuncval  9185  tskmval  9282  peano5uzti  11048  uzval  11184  reexALT  11319  ixxval  11668  fzval  11812  hashbclem  12656  hashbc  12657  shftfn  13213  rpnnen  14356  bitsfval  14475  sadfval  14505  sadcom  14516  smufval  14530  smupp1  14533  smupval  14541  smumullem  14545  gcdval  14549  bezoutlem2OLD  14583  bezoutlem4OLD  14585  bezoutlem2  14586  bezoutlem4  14588  lcmval  14634  lcmvalOLD  14635  lcmslefacOLD  14665  lcmfval  14670  lcmf0val  14671  lcmfvalOLD  14674  lcmfpr  14679  isprm  14703  isprm2lem  14710  odzval  14815  odzvalOLD  14821  pcval  14873  pceulem  14874  pceu  14875  pczpre  14876  pcdiv  14881  prmreclem1  14939  prmreclem4  14942  prmreclem5  14943  ramval  15039  ramvalOLD  15040  prmgaplcmlem1OLD  15091  prmordvdslcmsOLDOLD  15100  prmorlelcmsOLDOLD  15101  cshws0  15150  imasdsval  15494  imasdsvalOLD  15506  mrcval  15594  eldmcoa  16038  cycsubg2  16932  cntzval  17053  cntzsnval  17056  odfval  17257  odval  17258  odfvalOLD  17260  odvalOLD  17261  gexval  17305  gexvalOLD  17307  efgsfo  17467  dprdval  17713  ablfac1a  17780  ablfac1b  17781  ablfac1eu  17784  ablfaclem1  17796  ablfaclem3  17798  lspval  18276  aspval  18629  psrass1lem  18678  psrmulval  18687  mplmonmul  18765  coe1mul2  18939  ocvval  19307  dsmmelbas  19379  frlmsslss  19409  pmatcoe1fsupp  19802  istopon  20017  clsval  20129  neival  20195  ordtbaslem  20281  ordtbas2  20284  ordtopn1  20287  ordtopn2  20288  cnpval  20329  llyeq  20562  nllyeq  20563  ptfinfin  20611  finlocfin  20612  dissnlocfin  20621  locfindis  20622  xkoopn  20681  kqfval  20815  tsmsfbas  21220  blvalps  21478  blval  21479  nmofval  21797  nmoval  21798  nmofvalOLD  21816  nmovalOLD  21817  ishtpy  22081  minveclem3b  22448  minveclem3  22449  minveclem4  22452  minveclem5  22453  minveclem3bOLD  22460  minveclem3OLD  22461  minveclem4OLD  22464  minveclem5OLD  22465  ovolval  22504  ovolvalOLD  22505  vitalilem2  22646  vitalilem3  22647  vitalilem4  22648  vitali  22650  itg2monolem1  22787  elcpn  22967  mdegmullem  23106  elqaalem1  23351  elqaalem2  23352  elqaalem3  23353  elqaalem1OLD  23354  elqaalem2OLD  23355  elqaalem3OLD  23356  elqaa  23357  aannenlem1  23363  aannenlem2  23364  jensen  23993  vmaval  24119  muval  24138  sgmval  24148  fsumdvdscom  24193  musum  24199  muinv  24201  dchrisum0fval  24422  dchrisum0ff  24424  logsqvma2  24460  pntrlog2bndlem1  24494  tglngval  24675  ttgval  24984  ttgitvval  24991  ebtwntg  25091  nbgraopALT  25231  nbgraop1  25232  wwlkn  25489  clwwlkn  25574  hashecclwwlkn1  25641  usghashecclwwlk  25642  2wlkonot  25672  2spthonot  25673  2pthwlkonot  25692  vdgrval  25703  rusgraprop4  25751  rusgrasn  25752  rusgranumwwlkl1  25753  rusgranumwlklem1  25756  rusgranumwlklem3  25758  rusgranumwlks  25763  rusgranumwlkg  25765  eupath2  25787  usg2spot2nb  25872  usgreg2spot  25874  2spotmdisj  25875  usgreghash2spot  25876  numclwwlkdisj  25887  numclwwlk3lem  25915  numclwwlk5  25919  sspval  26443  ubthlem1  26593  ubthlem2  26594  ubthlem3  26595  ocval  27014  spanval  27067  chsupid  27146  eigvecval  27630  specval  27632  iunpreima  28257  aciunf1  28340  crefeq  28746  ordtcnvNEW  28800  ordtrest2NEW  28803  ordtconlem1  28804  measvuni  29110  brfae  29144  omsfval  29191  omsfvalOLD  29195  orvcelval  29374  ballotlemi  29406  ballotlemiOLD  29444  bnj602  29798  subfacp1lem6  29980  kur14  30011  cvmscbv  30053  cvmsi  30060  cvmsval  30061  snmlval  30126  snmlflim  30127  fvray  30979  fwddifnval  31001  neibastop3  31089  icoreval  31826  fin2so  31996  poimirlem26  32030  poimirlem27  32031  poimirlem28  32032  poimirlem32  32036  ftc1anclem6  32086  islinei  33376  pmapval  33393  paddval  33434  paddcom  33449  pclvalN  33526  ldilset  33745  dilsetN  33790  diafval  34670  diaval  34671  docavalN  34762  dicfval  34814  dochfval  34989  dochval  34990  mapdval  35267  mapdsn2  35281  2rexfrabdioph  35710  3rexfrabdioph  35711  4rexfrabdioph  35712  6rexfrabdioph  35713  7rexfrabdioph  35714  eldioph4i  35726  diophren  35727  pell1qrval  35763  pell14qrval  35765  pell1234qrval  35767  rpnnen3  35958  fnwe2lem1  35979  pwssplit4  36018  pwslnmlem2  36022  dgraaval  36076  dgraavalOLD  36077  itgoval  36098  rgspnval  36105  proot1hash  36148  nzss  36736  dvnprodlem1  37918  dvnprodlem2  37919  dvnprodlem3  37920  dvnprod  37921  stoweidlem26  37998  stoweidlem27  37999  stoweidlem31  38004  stoweidlem34  38007  stoweidlem46  38019  fourierdlem79  38161  fourierdlem96  38178  fourierdlem97  38179  fourierdlem98  38180  fourierdlem99  38181  fourierdlem105  38187  fourierdlem107  38189  fourierdlem108  38190  fourierdlem110  38192  etransclem11  38222  salgenval  38294  ovnval  38481  ovnval2  38485  ovnval2b  38492  ovncvrrp  38504  ovnsubaddlem1  38510  ovnsubadd  38512  ovncvr2  38551  hspmbl  38569  ovolval2  38584  ovnovollem3  38598  dfnbgr2  39571  dfnbgr3  39572  uvtxusgr  39639  vtxdgval  39694  eupth2  40151  rnghmval  40399  bigoval  40868