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

Theorem rabbidv 2940
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 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  ch ) )
32rabbidva 2939 1  |-  ( ph  ->  { x  e.  A  |  ps }  =  {
x  e.  A  |  ch } )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1652    e. wcel 1725   {crab 2701
This theorem is referenced by:  rabeqbidv  2943  difeq2  3451  seex  4537  mptiniseg  5355  fineqvlem  7314  supeq1  7441  supeq2  7444  oieq1  7470  oieq2  7471  ordtypecbv  7475  ordtypelem3  7478  harval  7519  inf3lema  7568  wemapwe  7643  oef1o  7644  tz9.12lem3  7704  rankvalb  7712  rankvalg  7732  ranksnb  7742  rankonidlem  7743  cardval3  7828  cardidm  7835  alephsuc2  7950  coftr  8142  fin1a2lem11  8279  fin1a2lem12  8280  hsmex  8301  axdc3lem2  8320  zorn2lem1  8365  zorn2lem6  8370  zorn2lem7  8371  zorn2g  8372  wuncval  8606  tskmval  8703  peano5uzti  10348  uzval  10479  reexALT  10595  ixxval  10913  fzval  11034  hashbclem  11689  hashbc  11690  shftfn  11876  rpnnen  12814  bitsfval  12923  sadfval  12952  sadcom  12963  smufval  12977  smupp1  12980  smupval  12988  smumullem  12992  gcdval  12996  bezoutlem2  13027  bezoutlem4  13029  isprm  13069  isprm2lem  13074  odzval  13165  pcval  13206  pceulem  13207  pceu  13208  pczpre  13209  pcdiv  13214  prmreclem1  13272  prmreclem4  13275  prmreclem5  13276  ramval  13364  imasdsval  13729  mrcval  13823  eldmcoa  14208  cycsubg2  14965  cntzval  15108  cntzsnval  15111  odfval  15159  odval  15160  gexval  15200  efgsfo  15359  dprdval  15549  ablfac1a  15615  ablfac1b  15616  ablfac1eu  15619  ablfaclem1  15631  ablfaclem3  15633  lspval  16039  aspval  16375  psrass1lem  16430  psrmulval  16438  mplmonmul  16515  coe1mul2  16650  ocvval  16882  istopon  16978  clsval  17089  neival  17154  ordtbaslem  17240  ordtbas2  17243  ordtopn1  17246  ordtopn2  17247  cnpval  17288  llyeq  17521  nllyeq  17522  xkoopn  17609  kqfval  17743  tsmsfbas  18145  blvalps  18403  blval  18404  nmofval  18736  nmoval  18737  ishtpy  18985  minveclem3b  19317  minveclem3  19318  minveclem4  19321  minveclem5  19322  ovolval  19358  vitalilem2  19489  vitalilem3  19490  vitalilem4  19491  vitali  19493  itg2monolem1  19630  elcpn  19808  mdegmullem  19989  elqaalem1  20224  elqaalem2  20225  elqaalem3  20226  elqaa  20227  aannenlem1  20233  aannenlem2  20234  jensen  20815  vmaval  20884  muval  20903  sgmval  20913  fsumdvdscom  20958  musum  20964  muinv  20966  dchrisum0fval  21187  dchrisum0ff  21189  logsqvma2  21225  pntrlog2bndlem1  21259  nbgraop1  21425  vdgrval  21655  eupath2  21690  sspval  22210  ubthlem1  22360  ubthlem2  22361  ubthlem3  22362  ocval  22770  spanval  22823  chsupid  22902  eigvecval  23387  specval  23389  measvuni  24556  brfae  24587  orvcelval  24714  ballotlemi  24746  subfacp1lem6  24859  kur14  24890  cvmscbv  24933  cvmsi  24940  cvmsval  24941  snmlval  25006  snmlflim  25007  fvray  26023  ptfinfin  26315  finlocfin  26316  locfindis  26322  neibastop3  26328  2rexfrabdioph  26793  3rexfrabdioph  26794  4rexfrabdioph  26795  6rexfrabdioph  26796  7rexfrabdioph  26797  eldioph4i  26810  diophren  26811  pell1qrval  26846  pell14qrval  26848  pell1234qrval  26850  rpnnen3  27040  fnwe2lem1  27062  pwssplit4  27106  pwslnmlem2  27110  dsmmelbas  27120  frlmsslss  27159  mapfien2  27173  dgraaval  27264  itgoval  27281  rgspnval  27288  proot1hash  27434  stoweidlem26  27689  stoweidlem27  27690  stoweidlem31  27694  stoweidlem34  27697  stoweidlem46  27709  2wlkonot  28206  2spthonot  28207  usg2spot2nb  28312  usgreg2spot  28314  2spotmdisj  28315  usgreghash2spot  28316  bnj602  29140  islinei  30376  pmapval  30393  paddval  30434  paddcom  30449  pclvalN  30526  ldilset  30745  dilsetN  30789  diafval  31668  diaval  31669  docavalN  31760  dicfval  31812  dochfval  31987  dochval  31988  mapdval  32265  mapdsn2  32279
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-ral 2702  df-rab 2706
  Copyright terms: Public domain W3C validator