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

Theorem iotabii 6112
 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 6099 . 2 (∀𝑥(𝜑𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
2 iotabii.1 . 2 (𝜑𝜓)
31, 2mpg 1896 1 (℩𝑥𝜑) = (℩𝑥𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 198   = wceq 1656  ℩cio 6088 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-uni 4661  df-iota 6090 This theorem is referenced by:  riotav  6876  ovtpos  7637  cbvsum  14809  cbvprod  15025  oppgid  18143  oppr1  18995  fourierdlem89  41200  fourierdlem90  41201  fourierdlem91  41202  fourierdlem96  41207  fourierdlem97  41208  fourierdlem98  41209  fourierdlem99  41210  fourierdlem100  41211  fourierdlem112  41223
 Copyright terms: Public domain W3C validator