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

Theorem iotabii 5579
Description: Formula-building deduction rule for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypothesis
Ref Expression
iotabii.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
iotabii  |-  ( iota
x ph )  =  ( iota x ps )

Proof of Theorem iotabii
StepHypRef Expression
1 iotabi 5566 . 2  |-  ( A. x ( ph  <->  ps )  ->  ( iota x ph )  =  ( iota x ps ) )
2 iotabii.1 . 2  |-  ( ph  <->  ps )
31, 2mpg 1667 1  |-  ( iota
x ph )  =  ( iota x ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    = wceq 1437   iotacio 5555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-rex 2779  df-uni 4214  df-iota 5557
This theorem is referenced by:  riotav  6264  ovtpos  6988  cbvsum  13739  cbvprod  13947  oppgid  16985  oppr1  17840  fourierdlem89  37846  fourierdlem90  37847  fourierdlem91  37848  fourierdlem96  37853  fourierdlem97  37854  fourierdlem98  37855  fourierdlem99  37856  fourierdlem100  37857  fourierdlem112  37869
  Copyright terms: Public domain W3C validator