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

Theorem abbidv 2593
Description: Equivalent wff's yield equal class abstractions (deduction rule). (Contributed by NM, 10-Aug-1993.)
Hypothesis
Ref Expression
abbidv.1
Assertion
Ref Expression
abbidv
Distinct variable group:   ,

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1707 . 2
2 abbidv.1 . 2
31, 2abbid 2592 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  {cab 2442
This theorem is referenced by:  rabbidva2  3099  cdeqab  3317  sbceqbid  3334  csbeq1  3437  csbeq2  3438  csbprc  3821  sbcel12  3823  sbcel12gOLD  3824  sbceqg  3825  csbeq2d  3834  csbnestgf  3840  pweq  4015  sneq  4039  csbsng  4088  rabsn  4097  unieq  4257  csbuni  4277  csbunigOLD  4278  inteq  4289  iineq1  4345  iineq2  4348  dfiin2g  4363  iinrab  4392  iinxprg  4408  opabbid  4514  csbxpgOLD  5087  imasng  5364  csbrngOLD  5474  iotaeq  5564  iotabi  5565  dfimafn  5922  fnsnfv  5933  fliftf  6213  oprabbid  6350  recseq  7062  rdglim2  7117  qseq1  7380  qseq2  7381  qsinxp  7406  mapvalg  7449  ixpsnval  7492  ixpeq1  7500  fival  7892  tcvalg  8190  karden  8334  acneq  8445  infmap2  8619  cfval  8648  cflim3  8663  axdclem  8920  axdc  8922  rankcf  9176  genpv  9398  hashf1lem2  12505  hashf1  12506  hashfac  12507  csbwrdg  12570  shftlem  12901  shftfib  12905  vdwlem6  14504  cshwsiun  14584  lubfval  15608  glbfval  15621  eqglact  16252  isghm  16267  symgval  16404  sylow1lem2  16619  sylow3lem1  16647  efgval  16735  dmdprd  17029  ixpsnbasval  17855  aspval2  17996  ressmplbas2  18117  cssval  18713  tgval  19456  clsval2  19551  lpfval  19639  lpval  19640  islocfin  20018  ptval  20071  hauspwpwf1  20488  ptcmplem2  20553  snclseqg  20614  ustval  20705  itg2val  22135  limcfval  22276  plyval  22590  isismt  23921  nbgraf1olem5  24445  nb3graprlem1  24451  fargshiftfo  24638  wwlknprop  24686  wwlknfi  24738  eclclwwlkn1  24832  rusgranumwlkb0  24953  rusgra0edg  24955  avril1  25171  elghomlem1OLD  25363  nmoofval  25677  nmooval  25678  nmoo0  25706  nmopval  26775  nmfnval  26795  iunrdx  27431  disjabrex  27443  disjabrexf  27444  dfimafnf  27473  curry2ima  27526  pstmval  27874  pstmfval  27875  sigaval  28110  measval  28169  orvcval  28396  derangval  28611  mclsval  28923  dfrtrcl2  29071  dfrdg2  29228  dfrdg3  29229  wrecseq123  29337  altxpeq1  29623  altxpeq2  29624  supadd  30042  ptrest  30048  mblfinlem3  30053  cnambfre  30063  itg2addnc  30069  areacirclem5  30111  sdclem2  30235  sdc  30237  ismtyval  30296  iineq12f  30573  eldiophb  30690  eldioph  30691  diophrw  30692  eldioph2  30695  eldioph2b  30696  eldioph3  30699  diophin  30706  diophun  30707  diophrex  30709  rexrabdioph  30727  rmxypairf1o  30847  hbtlem1  31072  hbtlem7  31074  nzss  31222  dropab1  31356  dropab2  31357  dfaimafn  32250  rnfdmpr  32308  csbfv12gALTOLD  33621  bnj956  33835  bnj18eq1  33985  bnj1318  34081  bj-snsetex  34521  bj-sngleq  34525  bj-projeq  34550  bj-projval  34554  lfl1dim  34846  ldual1dim  34891  glbconxN  35102  lineset  35462  pointsetN  35465  psubspset  35468  pmapglb2xN  35496  polval2N  35630  psubclsetN  35660  lautset  35806  pautsetN  35822  tendofset  36484  tendoset  36485  dva1dim  36711  dia1dim2  36789  dib1dim2  36895  diclspsn  36921  dih1dimatlem  37056  dihglb2  37069  hdmap1ffval  37523  hdmapffval  37556  hgmapffval  37615
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452
  Copyright terms: Public domain W3C validator