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

Theorem abbidv 2536
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 1664 . 2
2 abbidv.1 . 2
31, 2abbid 2535 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 178  =wceq 1687  {cab 2408
This theorem is referenced by:  rabbidva2  2941  cdeqab  3154  csbeq1  3268  csbeq2  3269  csbprc  3650  sbcel12  3652  sbcel12gOLD  3653  sbceqg  3654  csbeq2d  3663  csbnestgf  3669  pweq  3840  sneq  3864  csbsng  3912  rabsn  3919  unieq  4074  csbuni  4094  csbunigOLD  4095  inteq  4106  iineq1  4160  iineq2  4163  dfiin2g  4178  iinrab  4207  iinxprg  4223  opabbid  4329  csbxpgOLD  4890  imasng  5163  csbrngOLD  5272  iotaeq  5361  iotabi  5362  dfimafn  5710  fnsnfv  5721  fliftf  5976  oprabbid  6109  extmptsuppeq  6679  recseq  6792  rdglim2  6847  qseq1  7111  qseq2  7112  qsinxp  7137  mapvalg  7185  ixpsnval  7225  ixpeq1  7233  fival  7609  tcvalg  7905  karden  8049  acneq  8160  dfac2a  8246  infmap2  8334  cfval  8363  cflim3  8378  axdclem  8635  axdc  8637  rankcf  8890  genpv  9114  hashbclem  12146  hashf1lem2  12150  hashf1  12151  hashfac  12152  csbwrdg  12198  wrdlenfi  12199  shftlem  12498  shftfib  12502  vdwlem6  13987  cshwsiun  14066  lubfval  15088  glbfval  15101  eqglact  15669  isghm  15684  symgval  15821  sylow1lem2  16035  sylow3lem1  16063  efgval  16151  dmdprd  16368  ixpsnbasval  17099  aspval2  17225  ressmplbas2  17341  cssval  17815  tgval  18264  clsval2  18358  lpfval  18446  lpval  18447  ptval  18847  hauspwpwf1  19264  ptcmplem2  19329  snclseqg  19390  ustval  19477  itg2val  20906  limcfval  21047  plyval  21402  isusgra0  22954  nbgraf1olem5  23033  nb3graprlem1  23038  fargshiftfo  23203  avril1  23335  elghomlem1  23527  nmoofval  23841  nmooval  23842  nmoo0  23870  nmopval  24939  nmfnval  24959  sbceqbid  25544  iunrdx  25594  disjabrex  25606  disjabrexf  25607  dfimafnf  25630  curry2ima  25683  pstmval  26031  pstmfval  26032  sigaval  26262  measval  26321  orvcval  26543  derangval  26758  dfrtrcl2  27052  dfrdg2  27311  dfrdg3  27312  wrecseq123  27420  altxpeq1  27706  altxpeq2  27707  supadd  28089  ptrest  28096  mblfinlem3  28101  cnambfre  28111  itg2addnc  28117  areacirclem5  28159  islocfin  28239  sdclem2  28309  sdc  28311  ismtyval  28370  iineq12f  28648  eldiophb  28768  eldioph  28769  diophrw  28770  eldioph2  28773  eldioph2b  28774  eldioph3  28777  diophin  28784  diophun  28785  diophrex  28787  rexrabdioph  28805  rmxypairf1o  28925  hbtlem1  29152  hbtlem7  29154  dropab1  29376  dropab2  29377  dfaimafn  29745  rnfdmpr  29823  wwlknprop  29994  wwlkextwrd  30034  wwlknfi  30044  eclclwwlkn1  30180  rusgranumwlkl1  30233  rusgranumwlklem3  30243  rusgranumwlkb0  30245  rusgra0edg  30247  numclwwlkovf2  30351  csbfv12gALTOLD  31135  bnj956  31348  bnj18eq1  31498  bnj1318  31594  bj-snsetex  31903  bj-sngleq  31907  bj-projeq  31932  bj-projval  31936  lfl1dim  32203  ldual1dim  32248  glbconxN  32459  lineset  32819  pointsetN  32822  psubspset  32825  pmapglb2xN  32853  polval2N  32987  psubclsetN  33017  lautset  33163  pautsetN  33179  tendofset  33839  tendoset  33840  dva1dim  34066  dia1dim2  34144  dib1dim2  34250  diclspsn  34276  dih1dimatlem  34411  dihglb2  34424  mapdvalc  34711  mapdval4N  34714  hdmap1ffval  34878  hdmapffval  34911  hgmapffval  34970
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403
This theorem depends on definitions:  df-bi 179  df-an 364  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415
  Copyright terms: Public domain W3C validator