Theorem iotabii 6477

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

Syntax hints:   ↔ wb 206   = wceq 1542  ℩cio 6446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-uni 4852  df-iota 6448

This theorem is referenced by:  riotav  7322  riotarab  7359  ovtpos  8184  cbvsum  15648  cbvsumv  15649  cbvprod  15869  cbvprodv  15870  prodeq1i  15872  oppgid  19322  oppr1  20321  riotaeqbii  36396  sumeq2si  36400  prodeq2si  36402  cbvprodvw2  36445  dfpre  38811  fourierdlem89  46641  fourierdlem90  46642  fourierdlem91  46643  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem100  46652  fourierdlem112  46664