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

Theorem rabbidva 3100
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 28-Nov-2003.)
Hypothesis
Ref Expression
rabbidva.1
Assertion
Ref Expression
rabbidva
Distinct variable group:   ,

Proof of Theorem rabbidva
StepHypRef Expression
1 rabbidva.1 . . 3
21ralrimiva 2871 . 2
3 rabbi 3036 . 2
42, 3sylib 196 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  {crab 2811
This theorem is referenced by:  rabbidv  3101  rabeqbidva  3105  rabbi2dva  3705  rabxfrd  4673  ordintdif  4932  seinxp  5071  f1oresrab  6063  onsucmin  6656  suppval1  6924  mptsuppd  6942  cantnflem1  8129  dfinfmr  10545  ixxin  11575  mptnn0fsuppr  12105  scshwfzeqfzo  12794  incexc2  13650  smueqlem  14140  gcdass  14183  pcneg  14397  ramval  14526  acsfn  15056  monpropd  15132  f1omvdcnv  16469  pmtrmvd  16481  submod  16589  odngen  16597  sylow3lem6  16652  efgsfo  16757  rrgsupp  17939  rrgsuppOLD  17940  mplsubglem2  18097  ltbwe  18137  coe1mul2lem2  18309  dsmmbas2  18768  dsmmacl  18772  frlmbas  18786  frlmbasOLD  18787  frlmsslss2  18805  frlmsslss2OLD  18806  scmatmats  19013  mretopd  19593  ordtbaslem  19689  ordtrest  19703  ordtrest2lem  19704  leordtval  19714  xkopt  20156  xkoco1cn  20158  xkoco2cn  20159  xkoinjcn  20188  r0cld  20239  utopsnneiplem  20750  stdbdbl  21020  minveclem3b  21843  minveclem4  21847  lhop1lem  22414  mumul  23455  sqff1o  23456  lgsquadlem1  23629  lgsquadlem2  23630  wwlkextprop  24744  vdgrun  24901  vdgrfiun  24902  rusgranumwlklem0  24948  rusgranumwlks  24956  frisusgranb  24997  extwwlkfab  25090  grpoidinv2  25220  grpoinv  25229  xppreima  27487  cnvordtrestixx  27895  ordtrestNEW  27903  ordtrest2NEWlem  27904  lineunray  29797  lineelsb2  29798  linecom  29800  ee7.2aOLD  29926  mbfposadd  30062  cnambfre  30063  itg2addnclem2  30067  iblabsnclem  30078  ftc1anclem1  30090  istopclsd  30632  diophren  30747  rabrenfdioph  30748  pwfi2f1o  31044  acsfn1p  31148  idomrootle  31152  idomodle  31153  hausgraph  31172  lcmass  31218  nzss  31222  rmsupp0  32961  lco0  33028  lfl1dim2N  34847  pmapat  35487  pmapglbx  35493  dvhb1dimN  36712  dia0  36779  mapdval2N  37357  mapdsn  37368  hlhilocv  37687
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  df-ral 2812  df-rab 2816
  Copyright terms: Public domain W3C validator