MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iotabidv Structured version   Unicode version

Theorem iotabidv 5407
Description: Formula-building deduction rule for iota. (Contributed by NM, 20-Aug-2011.)
Hypothesis
Ref Expression
iotabidv.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
iotabidv  |-  ( ph  ->  ( iota x ps )  =  ( iota
x ch ) )
Distinct variable group:    ph, x
Allowed substitution hints:    ps( x)    ch( x)

Proof of Theorem iotabidv
StepHypRef Expression
1 iotabidv.1 . . 3  |-  ( ph  ->  ( ps  <->  ch )
)
21alrimiv 1685 . 2  |-  ( ph  ->  A. x ( ps  <->  ch ) )
3 iotabi 5395 . 2  |-  ( A. x ( ps  <->  ch )  ->  ( iota x ps )  =  ( iota
x ch ) )
42, 3syl 16 1  |-  ( ph  ->  ( iota x ps )  =  ( iota
x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1367    = wceq 1369   iotacio 5384
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-rex 2726  df-uni 4097  df-iota 5386
This theorem is referenced by:  csbiota  5415  csbiotagOLD  5416  dffv3  5692  fveq1  5695  fveq2  5696  fvres  5709  csbfv12  5730  csbfv12gOLD  5731  opabiota  5759  fvco2  5771  fvopab5  5800  riotaeqdv  6058  riotabidv  6059  riotabidva  6074  erov  7202  iunfictbso  8289  isf32lem9  8535  shftval  12568  sumeq1  13171  sumeq2w  13174  sumeq2ii  13175  zsum  13200  isumclim3  13231  isumshft  13307  pcval  13916  grpidval  15437  grpidpropd  15452  gsumvalx  15507  gsumpropd  15509  gsumpropd2lem  15510  gsumress  15512  psgnfval  16011  psgnval  16018  psgndif  18037  dchrptlem1  22608  lgsdchrval  22691  ajval  24267  adjval  25299  resv1r  26310  prodeq1f  27426  prodeq2w  27430  prodeq2ii  27431  zprod  27455  iprodclim3  27505  bj-finsumval0  32588
  Copyright terms: Public domain W3C validator