Theorem iotabii 6523

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

Step	Hyp	Ref	Expression
1		iotabi 6507	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
2		iotabii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1827	1 ⊢ (℩𝑥𝜑) = (℩𝑥𝜓)

Syntax hints:   ↔ wb 209   = wceq 1570  ℩cio 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-uni 4874  df-iota 6494

This theorem is referenced by:  riotav  7374  riotarab  7411  ovtpos  8238  cbvsum  15748  cbvsumv  15749  cbvprod  15969  cbvprodv  15970  prodeq1i  15972  oppgid  19427  oppr1  20433  riotaeqbii  36688  sumeq2si  36692  prodeq2si  36694  cbvprodvw2  36737  dfpre  39103  fourierdlem89  46889  fourierdlem90  46890  fourierdlem91  46891  fourierdlem96  46896  fourierdlem97  46897  fourierdlem98  46898  fourierdlem99  46899  fourierdlem100  46900  fourierdlem112  46912