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

Theorem iotabii 6324
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 6311 . 2 (∀𝑥(𝜑𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
2 iotabii.1 . 2 (𝜑𝜓)
31, 2mpg 1804 1 (℩𝑥𝜑) = (℩𝑥𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1542  cio 6295
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-in 3850  df-ss 3860  df-uni 4797  df-iota 6297
This theorem is referenced by:  riotav  7132  ovtpos  7936  cbvsum  15145  cbvprod  15361  oppgid  18602  oppr1  19506  riotarab  33246  fourierdlem89  43278  fourierdlem90  43279  fourierdlem91  43280  fourierdlem96  43285  fourierdlem97  43286  fourierdlem98  43287  fourierdlem99  43288  fourierdlem100  43289  fourierdlem112  43301
  Copyright terms: Public domain W3C validator