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

Theorem rabbidva 3219
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 2995 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rabbi 3150 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
42, 3sylib 208 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  wral 2941  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-ral 2946  df-rab 2950
This theorem is referenced by:  rabbidv  3220  rabeqbidva  3227  rabbi2dva  3854  rabxfrd  4919  seinxp  5219  ordintdif  5812  f1oresrab  6435  onsucmin  7063  suppval1  7346  mptsuppd  7363  cantnflem1  8624  dfinfre  11042  ixxin  12230  mptnn0fsuppr  12839  scshwfzeqfzo  13618  incexc2  14614  smueqlem  15259  gcdass  15311  lcmass  15374  pcneg  15625  ramval  15759  acsfn  16367  monpropd  16444  f1omvdcnv  17910  pmtrmvd  17922  submod  18030  odngen  18038  sylow3lem6  18093  efgsfo  18198  rrgsupp  19339  mplsubglem2  19484  ltbwe  19520  coe1mul2lem2  19686  dsmmbas2  20129  dsmmacl  20133  frlmbas  20147  frlmsslss2  20162  scmatmats  20365  mretopd  20944  ordtbaslem  21040  ordtrest  21054  ordtrest2lem  21055  leordtval  21065  xkopt  21506  xkoco1cn  21508  xkoco2cn  21509  xkoinjcn  21538  r0cld  21589  utopsnneiplem  22098  stdbdbl  22369  minveclem3b  23245  minveclem4  23249  lhop1lem  23821  mumul  24952  sqff1o  24953  lgsquadlem1  25150  lgsquadlem2  25151  2lgslem1a  25161  edglnl  26083  nbupgr  26285  isuvtxaOLD  26344  vtxdun  26433  wwlksnextprop  26875  wpthswwlks2on  26927  wpthswwlks2onOLD  26928  rusgrnumwwlkslem  26936  rusgrnumwwlks  26941  frcond3  27249  extwwlkfab  27342  grpoidinv2  27497  grpoinv  27507  xppreima  29577  cnvordtrestixx  30087  ordtrestNEW  30095  ordtrest2NEWlem  30096  lineunray  32379  lineelsb2  32380  linecom  32382  ee7.2aOLD  32585  poimirlem26  33565  poimirlem27  33566  mbfposadd  33587  cnambfre  33588  itg2addnclem2  33592  iblabsnclem  33603  ftc1anclem1  33615  lfl1dim2N  34727  pmapat  35367  pmapglbx  35373  dvhb1dimN  36591  dia0  36658  mapdval2N  37236  mapdsn  37247  hlhilocv  37566  istopclsd  37580  diophren  37694  rabrenfdioph  37695  pwfi2f1o  37983  acsfn1p  38086  idomrootle  38090  idomodle  38091  hausgraph  38107  fsovcnvlem  38624  ntrneifv3  38697  ntrneifv4  38700  clsneifv3  38725  clsneifv4  38726  neicvgfv  38736  nzss  38833  preimaiocmnf  40106  preimaicomnf  41243  smfsupxr  41343  smfliminflem  41357  sprvalpwle2  42064  rmsupp0  42474  lco0  42541
  Copyright terms: Public domain W3C validator