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

Theorem abbidv 2579
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 1694 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2578 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383   {cab 2428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438
This theorem is referenced by:  rabbidva2  3085  cdeqab  3303  sbceqbid  3320  csbeq1  3423  csbeq2  3424  csbprc  3807  sbcel12  3809  sbcel12gOLD  3810  sbceqg  3811  csbeq2d  3820  csbnestgf  3826  pweq  4000  sneq  4024  csbsng  4073  rabsn  4082  unieq  4242  csbuni  4262  csbunigOLD  4263  inteq  4274  iineq1  4330  iineq2  4333  dfiin2g  4348  iinrab  4377  iinxprg  4393  opabbid  4499  csbxpgOLD  5072  imasng  5349  csbrngOLD  5459  iotaeq  5549  iotabi  5550  dfimafn  5907  fnsnfv  5918  fliftf  6198  oprabbid  6335  recseq  7045  rdglim2  7100  qseq1  7363  qseq2  7364  qsinxp  7389  mapvalg  7432  ixpsnval  7474  ixpeq1  7482  fival  7874  tcvalg  8172  karden  8316  acneq  8427  infmap2  8601  cfval  8630  cflim3  8645  axdclem  8902  axdc  8904  rankcf  9158  genpv  9380  hashf1lem2  12487  hashf1  12488  hashfac  12489  csbwrdg  12552  shftlem  12883  shftfib  12887  vdwlem6  14486  cshwsiun  14566  lubfval  15587  glbfval  15600  eqglact  16231  isghm  16246  symgval  16383  sylow1lem2  16598  sylow3lem1  16626  efgval  16714  dmdprd  17008  ixpsnbasval  17834  aspval2  17975  ressmplbas2  18096  cssval  18691  tgval  19434  clsval2  19529  lpfval  19617  lpval  19618  islocfin  19996  ptval  20049  hauspwpwf1  20466  ptcmplem2  20531  snclseqg  20592  ustval  20683  itg2val  22113  limcfval  22254  plyval  22568  isismt  23899  nbgraf1olem5  24423  nb3graprlem1  24429  fargshiftfo  24616  wwlknprop  24664  wwlknfi  24716  eclclwwlkn1  24810  rusgranumwlkb0  24931  rusgra0edg  24933  avril1  25149  elghomlem1OLD  25341  nmoofval  25655  nmooval  25656  nmoo0  25684  nmopval  26753  nmfnval  26773  iunrdx  27409  disjabrex  27421  disjabrexf  27422  dfimafnf  27451  curry2ima  27504  pstmval  27852  pstmfval  27853  sigaval  28088  measval  28147  orvcval  28374  derangval  28589  mclsval  28901  dfrtrcl2  29049  dfrdg2  29204  dfrdg3  29205  wrecseq123  29313  altxpeq1  29599  altxpeq2  29600  supadd  30018  ptrest  30024  mblfinlem3  30029  cnambfre  30039  itg2addnc  30045  areacirclem5  30087  sdclem2  30211  sdc  30213  ismtyval  30272  iineq12f  30549  eldiophb  30666  eldioph  30667  diophrw  30668  eldioph2  30671  eldioph2b  30672  eldioph3  30675  diophin  30682  diophun  30683  diophrex  30685  rexrabdioph  30703  rmxypairf1o  30823  hbtlem1  31048  hbtlem7  31050  nzss  31198  dropab1  31310  dropab2  31311  dfaimafn  32204  rnfdmpr  32262  csbfv12gALTOLD  33489  bnj956  33703  bnj18eq1  33853  bnj1318  33949  bj-snsetex  34404  bj-sngleq  34408  bj-projeq  34433  bj-projval  34437  lfl1dim  34721  ldual1dim  34766  glbconxN  34977  lineset  35337  pointsetN  35340  psubspset  35343  pmapglb2xN  35371  polval2N  35505  psubclsetN  35535  lautset  35681  pautsetN  35697  tendofset  36359  tendoset  36360  dva1dim  36586  dia1dim2  36664  dib1dim2  36770  diclspsn  36796  dih1dimatlem  36931  dihglb2  36944  hdmap1ffval  37398  hdmapffval  37431  hgmapffval  37490
  Copyright terms: Public domain W3C validator