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

Theorem rabbidv 3414
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.)
Hypothesis
Ref Expression
rabbidv.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
rabbidv (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidv
StepHypRef Expression
1 rabbidv.1 . . 3 (𝜑 → (𝜓𝜒))
21adantr 482 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
32rabbidva 3413 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542  wcel 2107  {crab 3406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-rab 3407
This theorem is referenced by:  difeq2  4075  seex  5593  mptiniseg  6188  dfpred3g  6262  elovmporab  7590  elovmpt3rab1  7604  fineqvlem  9140  mapfien2  9279  supeq1  9315  supeq2  9318  supeq3  9319  oieq1  9382  oieq2  9383  ordtypecbv  9387  ordtypelem3  9390  harval  9430  inf3lema  9494  wemapwe  9567  oef1o  9568  tz9.12lem3  9659  rankvalb  9667  rankvalg  9687  ranksnb  9697  rankonidlem  9698  cardval3  9822  cardidm  9829  alephsuc2  9950  coftr  10143  fin1a2lem11  10280  fin1a2lem12  10281  hsmex  10302  axdc3lem2  10321  zorn2lem1  10366  zorn2lem6  10371  zorn2lem7  10372  zorn2g  10373  wuncval  10612  tskmval  10709  peano5uzti  12524  uzval  12698  rpnnen1  12837  ixxval  13201  fzval  13355  hashbclem  14277  hashbc  14278  shftfn  14892  bitsfval  16238  sadfval  16267  sadcom  16278  smufval  16292  smupp1  16295  smupval  16303  smumullem  16307  gcdval  16311  bezoutlem2  16356  bezoutlem4  16358  lcmval  16403  lcmfval  16432  lcmf0val  16433  lcmfpr  16438  isprm  16484  odzval  16598  pcval  16651  pceulem  16652  pceu  16653  pczpre  16654  pcdiv  16659  prmreclem1  16723  prmreclem4  16726  prmreclem5  16727  ramval  16815  cshws0  16909  imasdsval  17332  mrcval  17425  eldmcoa  17886  cycsubg2  18935  cntzval  19033  cntzsnval  19036  odfval  19246  odfvalALT  19247  odval  19248  gexval  19289  efgsfo  19450  dprdval  19711  ablfac1a  19777  ablfac1b  19778  ablfac1eu  19781  ablfaclem1  19793  ablfaclem3  19795  lspval  20359  ocvval  20994  dsmmelbas  21068  frlmsslss  21103  aspval  21199  psrass1lemOLD  21265  psrass1lem  21268  psrmulval  21277  mplmonmul  21359  mhpval  21452  mhpmulcl  21461  coe1mul2  21562  pmatcoe1fsupp  21972  istopon  22183  toponsspwpw  22193  clsval  22310  neival  22375  ordtbaslem  22461  ordtbas2  22464  ordtopn1  22467  ordtopn2  22468  cnpval  22509  llyeq  22743  nllyeq  22744  ptfinfin  22792  finlocfin  22793  dissnlocfin  22802  locfindis  22803  xkoopn  22862  kqfval  22996  tsmsfbas  23401  blvalps  23660  blval  23661  nmofval  24000  nmoval  24001  ishtpy  24257  minveclem3b  24714  minveclem3  24715  minveclem4  24718  minveclem5  24719  ovolval  24759  vitalilem2  24895  vitalilem3  24896  vitalilem4  24897  vitali  24899  itg2monolem1  25037  elcpn  25220  mdegmullem  25365  elqaalem1  25601  elqaalem2  25602  elqaalem3  25603  elqaa  25604  aannenlem1  25610  aannenlem2  25611  jensen  26260  vmaval  26384  muval  26403  sgmval  26413  fsumdvdscom  26456  musum  26462  muinv  26464  dchrisum0fval  26775  dchrisum0ff  26777  logsqvma2  26813  pntrlog2bndlem1  26847  scutval  27061  tglngval  27279  ttgval  27603  ttgvalOLD  27604  ttgitvval  27616  ebtwntg  27717  numedglnl  27881  dfnbgr2  28071  dfnbgr3  28072  uvtxusgr  28136  vtxdgval  28202  rusgrnumwrdl2  28320  iswwlksnon  28584  rusgrnumwwlks  28705  hashecclwwlkn1  28807  umgrhashecclwwlk  28808  clwlknf1oclwwlknlem2  28812  clwwlknon  28820  clwwlk0on0  28822  eupth2  28969  fusgreg2wsplem  29063  fusgreghash2wsp  29068  numclwlk1lem1  29099  sspval  29451  ubthlem1  29598  ubthlem2  29599  ubthlem3  29600  ocval  30008  spanval  30061  chsupid  30140  eigvecval  30624  specval  30626  iunpreima  31268  pwrssmgc  31642  nsgqusf1olem3  31974  crefeq  32187  zarcls1  32211  zarclsun  32212  zarclsiin  32213  zarclsint  32214  zarclssn  32215  zartop  32218  zartopon  32219  zart0  32221  zarmxt1  32222  zarcmp  32224  rhmpreimacnlem  32226  rhmpreimacn  32227  ordtcnvNEW  32262  ordtrest2NEW  32265  ordtconnlem1  32266  measvuni  32574  brfae  32608  omsfval  32655  orvcelval  32829  ballotlemi  32861  bnj602  33288  subfacp1lem6  33540  kur14  33571  cvmscbv  33613  cvmsi  33620  cvmsval  33621  snmlval  33686  snmlflim  33687  satfv0  33713  satfv1  33718  satfv0fun  33726  satffunlem1lem1  33757  satffunlem2lem1  33759  satfv0fvfmla0  33768  satfv1fvfmla1  33778  prv1n  33786  naddcllem  34208  naddov2  34211  naddcom  34214  naddid1  34215  naddass  34226  fvray  34612  fwddifnval  34634  neibastop3  34720  icoreval  35710  fin2so  35951  poimirlem26  35990  poimirlem27  35991  poimirlem28  35992  poimirlem32  35996  ftc1anclem6  36042  islinei  38089  pmapval  38106  paddval  38147  paddcom  38162  pclvalN  38239  ldilset  38458  dilsetN  38502  diafval  39380  diaval  39381  docavalN  39472  dicfval  39524  dochfval  39699  dochval  39700  mapdval  39977  mapdsn2  39991  prjcrvval  40804  2rexfrabdioph  40953  3rexfrabdioph  40954  4rexfrabdioph  40955  6rexfrabdioph  40956  7rexfrabdioph  40957  eldioph4i  40969  diophren  40970  pell1qrval  41003  pell14qrval  41005  pell1234qrval  41007  rpnnen3  41190  fnwe2lem1  41211  pwssplit4  41250  pwslnmlem2  41254  dgraaval  41305  itgoval  41322  rgspnval  41329  proot1hash  41361  rfovfvd  42005  rfovfvfvd  42006  rfovcnvf1od  42007  fsovrfovd  42012  fsovfvd  42013  fsovfvfvd  42014  fsovcnvlem  42016  nzss  42330  supminfxr  43413  dvnprodlem1  43897  dvnprodlem2  43898  dvnprodlem3  43899  dvnprod  43900  stoweidlem26  43977  stoweidlem27  43978  stoweidlem31  43982  stoweidlem34  43985  stoweidlem46  43997  fourierdlem79  44136  fourierdlem96  44153  fourierdlem97  44154  fourierdlem98  44155  fourierdlem99  44156  fourierdlem105  44162  fourierdlem107  44164  fourierdlem108  44165  fourierdlem110  44167  etransclem11  44196  salgenval  44272  subsaliuncl  44307  ovnval  44490  ovnval2  44494  ovnval2b  44501  ovncvrrp  44513  ovnsubaddlem1  44519  ovnsubadd  44521  ovncvr2  44560  hspmbl  44578  ovolval2  44593  ovnovollem3  44607  salpreimagelt  44656  salpreimalegt  44658  salpreimagtge  44674  salpreimaltle  44675  issmflem  44676  issmf  44677  salpreimagtlt  44679  smfpreimalt  44680  smfpreimaltf  44685  issmfle  44694  smfpimltxr  44696  smfpreimale  44703  issmfgt  44705  smfpreimagt  44711  issmfge  44719  smflimlem3  44722  smflimlem4  44723  smflim  44726  smfpimgtxr  44729  smfpreimage  44731  fvmptrabdm  45225  elsetpreimafveq  45289  prmdvdsfmtnof1  45479  fppr  45618  rnghmval  45889  bigoval  46335  line  46518  rrxline  46520  sphere  46533  line2y  46541  inpw  46603
  Copyright terms: Public domain W3C validator