Theorem iotabii 6485

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

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

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 6456

This theorem is referenced by:  riotav  7331  riotarab  7368  ovtpos  8193  cbvsum  15659  cbvsumv  15660  cbvprod  15880  cbvprodv  15881  prodeq1i  15883  oppgid  19333  oppr1  20332  riotaeqbii  36382  sumeq2si  36386  prodeq2si  36388  cbvprodvw2  36431  dfpre  38799  fourierdlem89  46625  fourierdlem90  46626  fourierdlem91  46627  fourierdlem96  46632  fourierdlem97  46633  fourierdlem98  46634  fourierdlem99  46635  fourierdlem100  46636  fourierdlem112  46648