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

Theorem iotabidv 5553
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 1740 . 2  |-  ( ph  ->  A. x ( ps  <->  ch ) )
3 iotabi 5541 . 2  |-  ( A. x ( ps  <->  ch )  ->  ( iota x ps )  =  ( iota
x ch ) )
42, 3syl 17 1  |-  ( ph  ->  ( iota x ps )  =  ( iota
x ch ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1403    = wceq 1405   iotacio 5530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-rex 2759  df-uni 4191  df-iota 5532
This theorem is referenced by:  csbiota  5561  dffv3  5844  fveq1  5847  fveq2  5848  fvres  5862  csbfv12  5883  opabiota  5911  fvco2  5923  fvopab5  5956  riotaeqdv  6240  riotabidv  6241  riotabidva  6255  erov  7444  iunfictbso  8526  isf32lem9  8772  shftval  13054  sumeq1  13658  sumeq2w  13661  sumeq2ii  13662  zsum  13687  isumclim3  13723  isumshft  13800  prodeq1f  13865  prodeq2w  13869  prodeq2ii  13870  zprod  13894  iprodclim3  13943  pcval  14575  grpidval  16209  grpidpropd  16210  gsumvalx  16219  gsumpropd  16221  gsumpropd2lem  16222  gsumress  16225  psgnfval  16847  psgnval  16854  psgndif  18934  dchrptlem1  23918  lgsdchrval  24001  ajval  26177  adjval  27208  resv1r  28266  bj-finsumval0  31214
  Copyright terms: Public domain W3C validator