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

Theorem rabbidva 3159
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:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem rabbidva
StepHypRef Expression
1 rabbidva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ralrimiva 2945 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rabbi 3093 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
42, 3sylib 206 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2892  {crab 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-ral 2897  df-rab 2901
This theorem is referenced by:  rabbidv  3160  rabeqbidva  3165  rabbi2dva  3779  rabxfrd  4807  seinxp  5095  ordintdif  5674  f1oresrab  6284  onsucmin  6887  suppval1  7162  mptsuppd  7179  cantnflem1  8443  dfinfre  10848  ixxin  12016  mptnn0fsuppr  12613  scshwfzeqfzo  13366  incexc2  14352  smueqlem  14993  gcdass  15045  lcmass  15108  pcneg  15359  ramval  15493  acsfn  16086  monpropd  16163  f1omvdcnv  17630  pmtrmvd  17642  submod  17750  odngen  17758  sylow3lem6  17813  efgsfo  17918  rrgsupp  19055  mplsubglem2  19200  ltbwe  19236  coe1mul2lem2  19402  dsmmbas2  19839  dsmmacl  19843  frlmbas  19857  frlmsslss2  19872  scmatmats  20075  mretopd  20645  ordtbaslem  20741  ordtrest  20755  ordtrest2lem  20756  leordtval  20766  xkopt  21207  xkoco1cn  21209  xkoco2cn  21210  xkoinjcn  21239  r0cld  21290  utopsnneiplem  21800  stdbdbl  22070  minveclem3b  22921  minveclem4  22925  lhop1lem  23494  mumul  24621  sqff1o  24622  lgsquadlem1  24819  lgsquadlem2  24820  2lgslem1a  24830  wwlkextprop  26035  vdgrun  26191  vdgrfiun  26192  rusgranumwlklem0  26238  rusgranumwlks  26246  frisusgranb  26287  extwwlkfab  26380  grpoidinv2  26516  grpoinv  26526  xppreima  28632  cnvordtrestixx  29090  ordtrestNEW  29098  ordtrest2NEWlem  29099  lineunray  31227  lineelsb2  31228  linecom  31230  ee7.2aOLD  31433  poimirlem26  32405  poimirlem27  32406  mbfposadd  32427  cnambfre  32428  itg2addnclem2  32432  iblabsnclem  32443  ftc1anclem1  32455  lfl1dim2N  33227  pmapat  33867  pmapglbx  33873  dvhb1dimN  35092  dia0  35159  mapdval2N  35737  mapdsn  35748  hlhilocv  36067  istopclsd  36081  diophren  36195  rabrenfdioph  36196  pwfi2f1o  36484  acsfn1p  36588  idomrootle  36592  idomodle  36593  hausgraph  36609  fsovcnvlem  37127  ntrneifv3  37200  ntrneifv4  37203  clsneifv3  37228  clsneifv4  37229  neicvgfv  37239  nzss  37338  preimaicomnf  39400  nbupgr  40565  isuvtxa  40620  vtxdun  40695  wwlksnextprop  41117  wpthswwlks2on  41163  rusgrnumwwlks  41176  frcond3  41439  av-extwwlkfab  41519  rmsupp0  41942  lco0  42009
  Copyright terms: Public domain W3C validator