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

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

Proof of Theorem rabbidva
StepHypRef Expression
1 rabbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ralrimiva 3113 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rabbi 3268 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
42, 3sylib 209 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1652  wcel 2155  wral 3055  {crab 3059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-ral 3060  df-rab 3064
This theorem is referenced by:  rabbidv  3338  rabeqbidva  3345  rabbi2dva  3981  rabxfrd  5052  seinxp  5355  ordintdif  5957  f1oresrab  6585  onsucmin  7219  suppval1  7503  mptsuppd  7520  cantnflem1  8801  dfinfre  11258  ixxin  12394  mptnn0fsuppr  13006  scshwfzeqfzo  13855  incexc2  14854  smueqlem  15493  gcdass  15545  lcmass  15608  pcneg  15857  ramval  15991  acsfn  16585  monpropd  16662  f1omvdcnv  18127  pmtrmvd  18139  submod  18248  odngen  18256  sylow3lem6  18311  efgsfo  18417  rrgsupp  19565  mplsubglem2  19710  ltbwe  19746  coe1mul2lem2  19911  dsmmbas2  20357  dsmmacl  20361  frlmbas  20375  frlmsslss2  20390  scmatmats  20594  mretopd  21176  ordtbaslem  21272  ordtrest  21286  ordtrest2lem  21287  leordtval  21297  xkopt  21738  xkoco1cn  21740  xkoco2cn  21741  xkoinjcn  21770  r0cld  21821  utopsnneiplem  22330  stdbdbl  22601  minveclem3b  23488  minveclem4  23492  lhop1lem  24067  mumul  25198  sqff1o  25199  lgsquadlem1  25396  lgsquadlem2  25397  2lgslem1a  25407  edglnl  26316  nbupgr  26519  isuvtxaOLD  26579  vtxdun  26668  wwlksnextprop  27130  wwlksnextpropOLD  27131  wpthswwlks2on  27185  wpthswwlks2onOLD  27186  rusgrnumwwlkslem  27194  rusgrnumwwlks  27199  rusgrnumwwlksOLD  27200  clwlknf1oclwwlknlem2  27348  clwlknf1oclwwlkn  27350  clwlknf1oclwwlknOLD  27352  frcond3  27549  extwwlkfab  27641  extwwlkfabOLD  27642  grpoidinv2  27826  grpoinv  27836  xppreima  29899  cnvordtrestixx  30406  ordtrestNEW  30414  ordtrest2NEWlem  30415  lineunray  32698  lineelsb2  32699  linecom  32701  ee7.2aOLD  32899  poimirlem26  33859  poimirlem27  33860  mbfposadd  33880  cnambfre  33881  itg2addnclem2  33885  iblabsnclem  33896  ftc1anclem1  33908  lfl1dim2N  35078  pmapat  35719  pmapglbx  35725  dvhb1dimN  36942  dia0  37008  mapdval2N  37586  mapdsn  37597  hlhilocv  37913  istopclsd  37941  diophren  38055  rabrenfdioph  38056  pwfi2f1o  38343  acsfn1p  38446  idomrootle  38450  idomodle  38451  hausgraph  38467  fsovcnvlem  38981  ntrneifv3  39054  ntrneifv4  39057  clsneifv3  39082  clsneifv4  39083  neicvgfv  39093  nzss  39190  preimaiocmnf  40426  preimaicomnf  41562  smfsupxr  41662  smfliminflem  41676  sprvalpwle2  42408  rmsupp0  42818  lco0  42885
  Copyright terms: Public domain W3C validator