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

Theorem rabbidva 3342
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 3118 . 2 (𝜑 → ∀𝑥𝐴 (𝜓𝜒))
3 rabbi 3273 . 2 (∀𝑥𝐴 (𝜓𝜒) ↔ {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
42, 3sylib 209 1 (𝜑 → {𝑥𝐴𝜓} = {𝑥𝐴𝜒})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 383   = wceq 1634  wcel 2148  wral 3064  {crab 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-ext 2754
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-clab 2761  df-cleq 2767  df-clel 2770  df-ral 3069  df-rab 3073
This theorem is referenced by:  rabbidv  3343  rabeqbidva  3350  rabbi2dva  3977  rabxfrd  5031  seinxp  5337  ordintdif  5928  f1oresrab  6555  onsucmin  7189  suppval1  7473  mptsuppd  7490  cantnflem1  8771  dfinfre  11227  ixxin  12416  mptnn0fsuppr  13028  scshwfzeqfzo  13803  incexc2  14799  smueqlem  15441  gcdass  15493  lcmass  15556  pcneg  15805  ramval  15939  acsfn  16547  monpropd  16624  f1omvdcnv  18091  pmtrmvd  18103  submod  18211  odngen  18219  sylow3lem6  18274  efgsfo  18379  rrgsupp  19526  mplsubglem2  19671  ltbwe  19707  coe1mul2lem2  19873  dsmmbas2  20318  dsmmacl  20322  frlmbas  20336  frlmsslss2  20351  scmatmats  20555  mretopd  21137  ordtbaslem  21233  ordtrest  21247  ordtrest2lem  21248  leordtval  21258  xkopt  21699  xkoco1cn  21701  xkoco2cn  21702  xkoinjcn  21731  r0cld  21782  utopsnneiplem  22291  stdbdbl  22562  minveclem3b  23438  minveclem4  23442  lhop1lem  24017  mumul  25149  sqff1o  25150  lgsquadlem1  25347  lgsquadlem2  25348  2lgslem1a  25358  edglnl  26281  nbupgr  26484  isuvtxaOLD  26544  vtxdun  26633  wwlksnextprop  27078  wpthswwlks2on  27130  wpthswwlks2onOLD  27131  rusgrnumwwlkslem  27139  rusgrnumwwlks  27144  clwlknf1oclwwlknlem2  27274  clwlknf1oclwwlkn  27276  frcond3  27472  extwwlkfab  27559  grpoidinv2  27726  grpoinv  27736  xppreima  29806  cnvordtrestixx  30316  ordtrestNEW  30324  ordtrest2NEWlem  30325  lineunray  32608  lineelsb2  32609  linecom  32611  ee7.2aOLD  32814  poimirlem26  33785  poimirlem27  33786  mbfposadd  33806  cnambfre  33807  itg2addnclem2  33811  iblabsnclem  33822  ftc1anclem1  33834  lfl1dim2N  34946  pmapat  35587  pmapglbx  35593  dvhb1dimN  36811  dia0  36877  mapdval2N  37455  mapdsn  37466  hlhilocv  37782  istopclsd  37804  diophren  37918  rabrenfdioph  37919  pwfi2f1o  38207  acsfn1p  38310  idomrootle  38314  idomodle  38315  hausgraph  38331  fsovcnvlem  38847  ntrneifv3  38920  ntrneifv4  38923  clsneifv3  38948  clsneifv4  38949  neicvgfv  38959  nzss  39056  preimaiocmnf  40312  preimaicomnf  41448  smfsupxr  41548  smfliminflem  41562  sprvalpwle2  42291  rmsupp0  42701  lco0  42768
  Copyright terms: Public domain W3C validator