Theorem abbidv 2741

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

Hypothesis

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

Assertion

Ref	Expression
abbidv	|- ( ph -> { x | ps } = { x | ch } )

Distinct variable group:   ph, x

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

Proof of Theorem abbidv

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 |- F/ x ph
2		abbidv.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	abbid 2740	1 |- ( ph -> { x | ps } = { x | ch } )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   {cab 2608

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

This theorem is referenced by:  rabbidva2  3186  cdeqab  3425  sbceqbid  3442  csbeq1  3536  csbeq2  3537  csbprc  3980  csbprcOLD  3981  sbcel12  3983  sbceqg  3984  csbeq2d  3991  csbnestgf  3996  pweq  4161  sneq  4187  csbsng  4243  rabsn  4256  unieq  4444  csbuni  4466  inteq  4478  iineq1  4535  iineq2  4538  dfiin2g  4553  iinrab  4582  iinxprg  4601  opabbid  4715  imasng  5487  iotaeq  5859  iotabi  5860  dfimafn  6245  fnsnfv  6258  fliftf  6565  oprabbid  6708  wrecseq123  7408  rdglim2  7528  qseq1  7796  qseq2  7797  qsinxp  7823  mapvalg  7867  ixpsnval  7911  ixpeq1  7919  fival  8318  tcvalg  8614  karden  8758  acneq  8866  infmap2  9040  cfval  9069  cflim3  9084  axdclem  9341  axdc  9343  rankcf  9599  genpv  9821  negfi  10971  supadd  10991  hashf1lem2  13240  hashf1  13241  hashfac  13242  csbwrdg  13334  cshimadifsn  13575  cshimadifsn0  13576  cleq1  13722  dfrtrcl2  13802  shftlem  13808  shftfib  13812  vdwlem6  15690  cshwsiun  15806  lubfval  16978  glbfval  16991  eqglact  17645  isghm  17660  symgval  17799  sylow1lem2  18014  sylow3lem1  18042  efgval  18130  dmdprd  18397  ixpsnbasval  19209  aspval2  19347  ressmplbas2  19455  cssval  20026  tgval  20759  clsval2  20854  lpfval  20942  lpval  20943  islocfin  21320  ptval  21373  hauspwpwf1  21791  ptcmplem2  21857  snclseqg  21919  ustval  22006  itg2val  23495  limcfval  23636  plyval  23949  isismt  25429  nb3grprlem1  26282  vtxdun  26377  rgrx0ndm  26489  ewlksfval  26497  wwlksnfi  26801  rusgrnumwwlkb0  26866  eclclwwlksn1  26952  avril1  27319  nmoofval  27617  nmooval  27618  nmoo0  27646  nmopval  28715  nmfnval  28735  iunrdx  29382  disjabrex  29395  disjabrexf  29396  dfimafnf  29436  curry2ima  29486  pstmval  29938  pstmfval  29939  sigaval  30173  measval  30261  orvcval  30519  bnj956  30847  bnj18eq1  30997  bnj1318  31093  derangval  31149  mclsval  31460  dfrdg2  31701  dfrdg3  31702  altxpeq1  32080  altxpeq2  32081  bj-snsetex  32951  bj-sngleq  32955  bj-projeq  32980  bj-projval  32984  csbwrecsg  33173  csboprabg  33176  finxpeq1  33223  finxpeq2  33224  csbfinxpg  33225  finxpreclem6  33233  ptrest  33408  poimirlem26  33435  poimirlem27  33436  poimirlem28  33437  mblfinlem3  33448  cnambfre  33458  itg2addnc  33464  areacirclem5  33504  sdclem2  33538  sdc  33540  ismtyval  33599  elghomlem1OLD  33684  iineq12f  33973  eccnvepres  34045  lfl1dim  34408  ldual1dim  34453  glbconxN  34664  lineset  35024  pointsetN  35027  psubspset  35030  pmapglb2xN  35058  polval2N  35192  psubclsetN  35222  lautset  35368  pautsetN  35384  tendofset  36046  tendoset  36047  dva1dim  36273  dia1dim2  36351  dib1dim2  36457  diclspsn  36483  dih1dimatlem  36618  dihglb2  36631  hdmap1ffval  37085  hdmapffval  37118  hgmapffval  37177  eldiophb  37320  eldioph  37321  diophrw  37322  eldioph2  37325  eldioph2b  37326  eldioph3  37329  diophin  37336  diophun  37337  diophrex  37339  rexrabdioph  37358  rmxypairf1o  37476  hbtlem1  37693  hbtlem7  37695  nzss  38516  dropab1  38651  dropab2  38652  sbcel12gOLD  38754  csbunigOLD  39051  csbfv12gALTOLD  39052  csbxpgOLD  39053  csbrngOLD  39056  supsubc  39569  dfaimafn  41245  rnfdmpr  41300  fargshiftfo  41378  sprval  41729  sprvalpw  41730  setrecseq  42432