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

Theorem iotabii 6545
Description: Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.)
Hypothesis
Ref Expression
iotabii.1 (𝜑𝜓)
Assertion
Ref Expression
iotabii (℩𝑥𝜑) = (℩𝑥𝜓)

Proof of Theorem iotabii
StepHypRef Expression
1 iotabi 6526 . 2 (∀𝑥(𝜑𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
2 iotabii.1 . 2 (𝜑𝜓)
31, 2mpg 1796 1 (℩𝑥𝜑) = (℩𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 206   = wceq 1539  cio 6511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-uni 4907  df-iota 6513
This theorem is referenced by:  riotav  7394  riotarab  7431  ovtpos  8267  cbvsum  15732  cbvsumv  15733  cbvprod  15950  cbvprodv  15951  prodeq1i  15953  oppgid  19376  oppr1  20351  riotaeqbii  36200  sumeq2si  36204  prodeq2si  36206  cbvprodvw2  36249  fourierdlem89  46215  fourierdlem90  46216  fourierdlem91  46217  fourierdlem96  46222  fourierdlem97  46223  fourierdlem98  46224  fourierdlem99  46225  fourierdlem100  46226  fourierdlem112  46238
  Copyright terms: Public domain W3C validator