Theorem iotabii 6471

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 6455	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓))
2		iotabii.1	. 2 ⊢ (𝜑 ↔ 𝜓)
3	1, 2	mpg 1798	1 ⊢ (℩𝑥𝜑) = (℩𝑥𝜓)

Syntax hints:   ↔ wb 206   = wceq 1541  ℩cio 6440

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-uni 4859  df-iota 6442

This theorem is referenced by:  riotav  7314  riotarab  7351  ovtpos  8177  cbvsum  15604  cbvsumv  15605  cbvprod  15822  cbvprodv  15823  prodeq1i  15825  oppgid  19270  oppr1  20270  riotaeqbii  36263  sumeq2si  36267  prodeq2si  36269  cbvprodvw2  36312  dfpre  38509  fourierdlem89  46317  fourierdlem90  46318  fourierdlem91  46319  fourierdlem96  46324  fourierdlem97  46325  fourierdlem98  46326  fourierdlem99  46327  fourierdlem100  46328  fourierdlem112  46340