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

Theorem iotabidv 5240
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 1617 . 2  |-  ( ph  ->  A. x ( ps  <->  ch ) )
3 iotabi 5228 . 2  |-  ( A. x ( ps  <->  ch )  ->  ( iota x ps )  =  ( iota
x ch ) )
42, 3syl 15 1  |-  ( ph  ->  ( iota x ps )  =  ( iota
x ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1527    = wceq 1623   iotacio 5217
This theorem is referenced by:  csbiotag  5248  dffv3  5521  fveq1  5524  fveq2  5525  csbfv12g  5535  fvres  5542  fvco2  5594  fvopab5  6289  opabiota  6293  riotaeqdv  6305  riotabidv  6306  riotabidva  6321  erov  6755  iunfictbso  7741  isf32lem9  7987  shftval  11569  sumeq1f  12161  sumeq2w  12165  sumeq2ii  12166  cbvsum  12168  zsum  12191  isumclim3  12222  isumshft  12298  pcval  12897  grpidval  14384  grpidpropd  14399  gsumvalx  14451  gsumpropd  14453  gsumress  14454  dchrptlem1  20503  lgsdchrval  20586  ajval  21440  adjval  22470  psgnfval  26835  psgnval  26842
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-uni 3828  df-iota 5219
  Copyright terms: Public domain W3C validator