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

Theorem iotabii 6528
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 6509 . 2 (∀𝑥(𝜑𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
2 iotabii.1 . 2 (𝜑𝜓)
31, 2mpg 1798 1 (℩𝑥𝜑) = (℩𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1540  cio 6493
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702
This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965  df-uni 4909  df-iota 6495
This theorem is referenced by:  riotav  7373  riotarab  7411  ovtpos  8232  cbvsum  15648  cbvprod  15866  oppgid  19271  oppr1  20248  fourierdlem89  45372  fourierdlem90  45373  fourierdlem91  45374  fourierdlem96  45379  fourierdlem97  45380  fourierdlem98  45381  fourierdlem99  45382  fourierdlem100  45383  fourierdlem112  45395
  Copyright terms: Public domain W3C validator