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

Theorem rabbidv 2780
Description: Equivalent wff's yield equal restricted class abstractions (deduction rule). (Contributed by NM, 10-Feb-1995.)
Hypothesis
Ref Expression
rabbidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
rabbidv  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)    A( x)

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21adantr 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32rabbidva 2779 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684   {crab 2547
This theorem is referenced by:  rabeqbidv  2783  difeq2  3288  seex  4356  mptiniseg  5167  fineqvlem  7077  supeq1  7198  supeq2  7201  oieq1  7227  oieq2  7228  ordtypecbv  7232  ordtypelem3  7235  harval  7276  inf3lema  7325  wemapwe  7400  oef1o  7401  tz9.12lem3  7461  rankvalb  7469  rankvalg  7489  ranksnb  7499  rankonidlem  7500  cardval3  7585  cardidm  7592  alephsuc2  7707  coftr  7899  fin1a2lem11  8036  fin1a2lem12  8037  hsmex  8058  axdc3lem2  8077  zorn2lem1  8123  zorn2lem6  8128  zorn2lem7  8129  zorn2g  8130  wuncval  8364  tskmval  8461  peano5uzti  10101  uzval  10232  reexALT  10348  ixxval  10664  fzval  10784  hashbclem  11390  hashbc  11391  shftfn  11568  rpnnen  12505  bitsfval  12614  sadfval  12643  sadcom  12654  smufval  12668  smupp1  12671  smupval  12679  smumullem  12683  gcdval  12687  bezoutlem2  12718  bezoutlem4  12720  isprm  12760  isprm2lem  12765  odzval  12856  pcval  12897  pceulem  12898  pceu  12899  pczpre  12900  pcdiv  12905  prmreclem1  12963  prmreclem4  12966  prmreclem5  12967  ramval  13055  imasdsval  13418  mrcval  13512  eldmcoa  13897  cycsubg2  14654  cntzval  14797  cntzsnval  14800  odfval  14848  odval  14849  gexval  14889  efgsfo  15048  dprdval  15238  ablfac1a  15304  ablfac1b  15305  ablfac1eu  15308  ablfaclem1  15320  ablfaclem3  15322  lspval  15732  aspval  16068  psrass1lem  16123  psrmulval  16131  mplmonmul  16208  coe1mul2  16346  ocvval  16567  istopon  16663  clsval  16774  neival  16839  ordtbaslem  16918  ordtbas2  16921  ordtopn1  16924  ordtopn2  16925  cnpval  16966  llyeq  17196  nllyeq  17197  xkoopn  17284  kqfval  17414  tsmsfbas  17810  blval  17948  nmofval  18223  nmoval  18224  ishtpy  18470  minveclem3b  18792  minveclem3  18793  minveclem4  18796  minveclem5  18797  ovolval  18833  vitalilem2  18964  vitalilem3  18965  vitalilem4  18966  vitali  18968  itg2monolem1  19105  elcpn  19283  mdegmullem  19464  elqaalem1  19699  elqaalem2  19700  elqaalem3  19701  elqaa  19702  aannenlem1  19708  aannenlem2  19709  jensen  20283  vmaval  20351  muval  20370  sgmval  20380  fsumdvdscom  20425  musum  20431  muinv  20433  dchrisum0fval  20654  dchrisum0ff  20656  logsqvma2  20692  pntrlog2bndlem1  20726  sspval  21299  ubthlem1  21449  ubthlem2  21450  ubthlem3  21451  ocval  21859  spanval  21912  chsupid  21991  eigvecval  22476  specval  22478  ballotlemi  23059  measvuni  23542  orvcelval  23669  subfacp1lem6  23716  kur14  23747  cvmscbv  23789  cvmsi  23796  cvmsval  23797  vdgrval  23890  eupath2  23904  snmlval  23914  snmlflim  23915  fvray  24764  ubos  25256  istopx  25547  istopxc  25548  ishomb  25788  cinvlem2  25829  sgplpte21  26132  sgplpte22  26138  isray2  26153  ptfinfin  26298  finlocfin  26299  locfindis  26305  neibastop3  26311  2rexfrabdioph  26877  3rexfrabdioph  26878  4rexfrabdioph  26879  6rexfrabdioph  26880  7rexfrabdioph  26881  eldioph4i  26895  diophren  26896  pell1qrval  26931  pell14qrval  26933  pell1234qrval  26935  rpnnen3  27125  fnwe2lem1  27147  pwssplit4  27191  pwslnmlem2  27195  dsmmelbas  27205  frlmsslss  27244  mapfien2  27258  dgraaval  27349  itgoval  27366  rgspnval  27373  proot1hash  27519  stoweidlem26  27775  stoweidlem27  27776  stoweidlem34  27783  stoweidlem46  27795  bnj602  28947  islinei  29929  pmapval  29946  paddval  29987  paddcom  30002  pclvalN  30079  ldilset  30298  dilsetN  30342  diafval  31221  diaval  31222  docavalN  31313  dicfval  31365  dochfval  31540  dochval  31541  mapdval  31818  mapdsn2  31832
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-ral 2548  df-rab 2552
  Copyright terms: Public domain W3C validator