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

Theorem abbidv 2590
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 1712 . 2  |-  F/ x ph
2 abbidv.1 . 2  |-  ( ph  ->  ( ps  <->  ch )
)
31, 2abbid 2589 1  |-  ( ph  ->  { x  |  ps }  =  { x  |  ch } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1398   {cab 2439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449
This theorem is referenced by:  rabbidva2  3096  cdeqab  3314  sbceqbid  3331  csbeq1  3423  csbeq2  3424  csbprc  3820  sbcel12  3822  sbceqg  3823  csbeq2d  3830  csbnestgf  3835  pweq  4002  sneq  4026  csbsng  4074  rabsn  4083  unieq  4243  csbuni  4263  inteq  4274  iineq1  4330  iineq2  4333  dfiin2g  4348  iinrab  4377  iinxprg  4396  opabbid  4501  imasng  5347  iotaeq  5542  iotabi  5543  dfimafn  5897  fnsnfv  5908  fliftf  6188  oprabbid  6323  recseq  7035  rdglim2  7090  qseq1  7353  qseq2  7354  qsinxp  7379  mapvalg  7422  ixpsnval  7465  ixpeq1  7473  fival  7864  tcvalg  8160  karden  8304  acneq  8415  infmap2  8589  cfval  8618  cflim3  8633  axdclem  8890  axdc  8892  rankcf  9144  genpv  9366  hashf1lem2  12492  hashf1  12493  hashfac  12494  csbwrdg  12561  cleq1  12904  dfrtrcl2  12980  shftlem  12986  shftfib  12990  vdwlem6  14591  cshwsiun  14671  lubfval  15810  glbfval  15823  eqglact  16454  isghm  16469  symgval  16606  sylow1lem2  16821  sylow3lem1  16849  efgval  16937  dmdprd  17227  ixpsnbasval  18053  aspval2  18194  ressmplbas2  18315  cssval  18889  tgval  19626  clsval2  19721  lpfval  19809  lpval  19810  islocfin  20187  ptval  20240  hauspwpwf1  20657  ptcmplem2  20722  snclseqg  20783  ustval  20874  itg2val  22304  limcfval  22445  plyval  22759  isismt  24125  nbgraf1olem5  24650  nb3graprlem1  24656  fargshiftfo  24843  wwlknprop  24891  wwlknfi  24943  eclclwwlkn1  25037  rusgranumwlkb0  25158  rusgra0edg  25160  avril1  25376  elghomlem1OLD  25564  nmoofval  25878  nmooval  25879  nmoo0  25907  nmopval  26976  nmfnval  26996  iunrdx  27644  disjabrex  27656  disjabrexf  27657  dfimafnf  27697  curry2ima  27758  pstmval  28112  pstmfval  28113  sigaval  28343  measval  28409  orvcval  28663  derangval  28878  mclsval  29190  dfrdg2  29471  dfrdg3  29472  wrecseq123  29580  altxpeq1  29854  altxpeq2  29855  supadd  30285  ptrest  30291  mblfinlem3  30296  cnambfre  30306  itg2addnc  30312  areacirclem5  30354  sdclem2  30478  sdc  30480  ismtyval  30539  iineq12f  30816  eldiophb  30932  eldioph  30933  diophrw  30934  eldioph2  30937  eldioph2b  30938  eldioph3  30941  diophin  30948  diophun  30949  diophrex  30951  rexrabdioph  30970  rmxypairf1o  31089  hbtlem1  31316  hbtlem7  31318  nzss  31466  dropab1  31600  dropab2  31601  dfaimafn  32492  rnfdmpr  32701  sbcel12gOLD  33724  csbunigOLD  34035  csbfv12gALTOLD  34036  csbxpgOLD  34037  csbrngOLD  34040  bnj956  34255  bnj18eq1  34405  bnj1318  34501  bj-snsetex  34941  bj-sngleq  34945  bj-projeq  34970  bj-projval  34974  lfl1dim  35262  ldual1dim  35307  glbconxN  35518  lineset  35878  pointsetN  35881  psubspset  35884  pmapglb2xN  35912  polval2N  36046  psubclsetN  36076  lautset  36222  pautsetN  36238  tendofset  36900  tendoset  36901  dva1dim  37127  dia1dim2  37205  dib1dim2  37311  diclspsn  37337  dih1dimatlem  37472  dihglb2  37485  hdmap1ffval  37939  hdmapffval  37972  hgmapffval  38031
  Copyright terms: Public domain W3C validator