MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abbidv Structured version   Visualization version   Unicode version

Theorem abbidv 2589
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
StepHypRef Expression
1 nfv 1769 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2588 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   {cab 2457
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
This theorem is referenced by:  rabbidva2  3020  cdeqab  3245  sbceqbid  3262  csbeq1  3352  csbeq2  3353  csbprc  3774  sbcel12  3776  sbceqg  3777  csbeq2d  3784  csbnestgf  3789  pweq  3945  sneq  3969  csbsng  4021  rabsn  4030  unieq  4198  csbuni  4218  inteq  4229  iineq1  4284  iineq2  4287  dfiin2g  4302  iinrab  4331  iinxprg  4350  opabbid  4458  imasng  5196  iotaeq  5561  iotabi  5562  dfimafn  5928  fnsnfv  5940  fliftf  6226  oprabbid  6363  wrecseq123  7047  rdglim2  7168  qseq1  7431  qseq2  7432  qsinxp  7457  mapvalg  7500  ixpsnval  7543  ixpeq1  7551  fival  7944  tcvalg  8240  karden  8384  acneq  8492  infmap2  8666  cfval  8695  cflim3  8710  axdclem  8967  axdc  8969  rankcf  9220  genpv  9442  negfi  10576  supadd  10597  hashf1lem2  12660  hashf1  12661  hashfac  12662  csbwrdg  12747  cshimadifsn  12985  cshimadifsn0  12986  cleq1  13122  dfrtrcl2  13202  shftlem  13208  shftfib  13212  vdwlem6  15015  cshwsiun  15148  lubfval  16302  glbfval  16315  eqglact  16946  isghm  16961  symgval  17098  sylow1lem2  17329  sylow3lem1  17357  efgval  17445  dmdprd  17708  ixpsnbasval  18510  aspval2  18648  ressmplbas2  18756  cssval  19322  tgval  20047  clsval2  20142  lpfval  20231  lpval  20232  islocfin  20609  ptval  20662  hauspwpwf1  21080  ptcmplem2  21146  snclseqg  21208  ustval  21295  itg2val  22765  limcfval  22906  plyval  23226  isismt  24658  nbgraf1olem5  25252  nb3graprlem1  25258  fargshiftfo  25445  wwlknprop  25493  wwlknfi  25545  eclclwwlkn1  25639  rusgranumwlkb0  25760  rusgra0edg  25762  avril1  25979  elghomlem1OLD  26170  nmoofval  26484  nmooval  26485  nmoo0  26513  nmopval  27590  nmfnval  27610  iunrdx  28256  disjabrex  28269  disjabrexf  28270  dfimafnf  28309  curry2ima  28364  pstmval  28772  pstmfval  28773  sigaval  29006  measval  29094  orvcval  29363  bnj956  29660  bnj18eq1  29810  bnj1318  29906  derangval  29962  mclsval  30273  dfrdg2  30513  dfrdg3  30514  altxpeq1  30811  altxpeq2  30812  bj-snsetex  31627  bj-sngleq  31631  bj-projeq  31656  bj-projval  31660  csbwrecsg  31798  csboprabg  31801  finxpeq1  31848  finxpeq2  31849  csbfinxpg  31850  finxpreclem6  31858  ptrest  32003  poimirlem26  32030  poimirlem27  32031  poimirlem28  32032  mblfinlem3  32043  cnambfre  32053  itg2addnc  32060  areacirclem5  32100  sdclem2  32135  sdc  32137  ismtyval  32196  iineq12f  32472  lfl1dim  32758  ldual1dim  32803  glbconxN  33014  lineset  33374  pointsetN  33377  psubspset  33380  pmapglb2xN  33408  polval2N  33542  psubclsetN  33572  lautset  33718  pautsetN  33734  tendofset  34396  tendoset  34397  dva1dim  34623  dia1dim2  34701  dib1dim2  34807  diclspsn  34833  dih1dimatlem  34968  dihglb2  34981  hdmap1ffval  35435  hdmapffval  35468  hgmapffval  35527  eldiophb  35670  eldioph  35671  diophrw  35672  eldioph2  35675  eldioph2b  35676  eldioph3  35679  diophin  35686  diophun  35687  diophrex  35689  rexrabdioph  35708  rmxypairf1o  35830  hbtlem1  36053  hbtlem7  36055  nzss  36736  dropab1  36870  dropab2  36871  sbcel12gOLD  36975  csbunigOLD  37275  csbfv12gALTOLD  37276  csbxpgOLD  37277  csbrngOLD  37280  supsubc  37663  dfaimafn  38812  rnfdmpr  39161  nb3grprlem1  39618  vtxdun  39704  rgrx0ndm  39797  ewlksfval  39807
  Copyright terms: Public domain W3C validator