MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abbidv 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
Assertion
Ref Expression
abbidv
Distinct variable group:   ,

Proof of Theorem abbidv
StepHypRef Expression
1 nfv 1674 . 2
2 abbidv.1 . 2
31, 2abbid 2589 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1370  {cab 2439
This theorem is referenced by:  rabbidva2  3071  cdeqab  3287  sbceqbid  3304  csbeq1  3404  csbeq2  3405  csbprc  3787  sbcel12  3789  sbcel12gOLD  3790  sbceqg  3791  csbeq2d  3800  csbnestgf  3806  pweq  3979  sneq  4003  csbsng  4052  rabsn  4059  unieq  4216  csbuni  4236  csbunigOLD  4237  inteq  4248  iineq1  4302  iineq2  4305  dfiin2g  4320  iinrab  4349  iinxprg  4365  opabbid  4471  csbxpgOLD  5036  imasng  5310  csbrngOLD  5419  iotaeq  5508  iotabi  5509  dfimafn  5863  fnsnfv  5874  fliftf  6139  oprabbid  6271  extmptsuppeq  6847  recseq  6967  rdglim2  7022  qseq1  7284  qseq2  7285  qsinxp  7310  mapvalg  7358  ixpsnval  7400  ixpeq1  7408  fival  7798  tcvalg  8095  karden  8239  acneq  8350  dfac2a  8436  infmap2  8524  cfval  8553  cflim3  8568  axdclem  8825  axdc  8827  rankcf  9081  genpv  9305  hashbclem  12363  hashf1lem2  12367  hashf1  12368  hashfac  12369  csbwrdg  12415  wrdlenfi  12416  shftlem  12715  shftfib  12719  vdwlem6  14205  cshwsiun  14284  lubfval  15307  glbfval  15320  eqglact  15891  isghm  15906  symgval  16043  sylow1lem2  16259  sylow3lem1  16287  efgval  16375  dmdprd  16655  ixpsnbasval  17466  aspval2  17593  ressmplbas2  17711  cssval  18300  tgval  18959  clsval2  19053  lpfval  19141  lpval  19142  ptval  19542  hauspwpwf1  19959  ptcmplem2  20024  snclseqg  20085  ustval  20176  itg2val  21606  limcfval  21747  plyval  22061  isismt  23385  isusgra0  23744  nbgraf1olem5  23823  nb3graprlem1  23828  fargshiftfo  23993  avril1  24125  elghomlem1  24317  nmoofval  24631  nmooval  24632  nmoo0  24660  nmopval  25729  nmfnval  25749  iunrdx  26382  disjabrex  26394  disjabrexf  26395  dfimafnf  26418  curry2ima  26470  pstmval  26779  pstmfval  26780  sigaval  27010  measval  27069  orvcval  27296  derangval  27511  dfrtrcl2  27806  dfrdg2  28065  dfrdg3  28066  wrecseq123  28174  altxpeq1  28460  altxpeq2  28461  supadd  28878  ptrest  28885  mblfinlem3  28890  cnambfre  28900  itg2addnc  28906  areacirclem5  28948  islocfin  29028  sdclem2  29098  sdc  29100  ismtyval  29159  iineq12f  29437  eldiophb  29555  eldioph  29556  diophrw  29557  eldioph2  29560  eldioph2b  29561  eldioph3  29564  diophin  29571  diophun  29572  diophrex  29574  rexrabdioph  29592  rmxypairf1o  29712  hbtlem1  29939  hbtlem7  29941  dropab1  30163  dropab2  30164  dfaimafn  30948  rnfdmpr  31026  wwlknprop  31197  wwlkextwrd  31237  wwlknfi  31247  eclclwwlkn1  31383  rusgranumwlkl1  31436  rusgranumwlklem3  31446  rusgranumwlkb0  31448  rusgra0edg  31450  numclwwlkovf2  31554  csbfv12gALTOLD  32400  bnj956  32613  bnj18eq1  32763  bnj1318  32859  bj-snsetex  33301  bj-sngleq  33305  bj-projeq  33330  bj-projval  33334  lfl1dim  33617  ldual1dim  33662  glbconxN  33873  lineset  34233  pointsetN  34236  psubspset  34239  pmapglb2xN  34267  polval2N  34401  psubclsetN  34431  lautset  34577  pautsetN  34593  tendofset  35253  tendoset  35254  dva1dim  35480  dia1dim2  35558  dib1dim2  35664  diclspsn  35690  dih1dimatlem  35825  dihglb2  35838  mapdvalc  36125  mapdval4N  36128  hdmap1ffval  36292  hdmapffval  36325  hgmapffval  36384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449
  Copyright terms: Public domain W3C validator