Theorem iotabii 6521

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

Syntax hints:   ↔ wb 206   = wceq 1540  ℩cio 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-ss 3948  df-uni 4889  df-iota 6489

This theorem is referenced by:  riotav  7372  riotarab  7409  ovtpos  8245  cbvsum  15716  cbvsumv  15717  cbvprod  15934  cbvprodv  15935  prodeq1i  15937  oppgid  19344  oppr1  20315  riotaeqbii  36221  sumeq2si  36225  prodeq2si  36227  cbvprodvw2  36270  fourierdlem89  46191  fourierdlem90  46192  fourierdlem91  46193  fourierdlem96  46198  fourierdlem97  46199  fourierdlem98  46200  fourierdlem99  46201  fourierdlem100  46202  fourierdlem112  46214