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 3444  df-ss 3920  df-uni 4866  df-iota 6456

This theorem is referenced by:  riotav  7330  riotarab  7367  ovtpos  8193  cbvsum  15630  cbvsumv  15631  cbvprod  15848  cbvprodv  15849  prodeq1i  15851  oppgid  19297  oppr1  20298  riotaeqbii  36411  sumeq2si  36415  prodeq2si  36417  cbvprodvw2  36460  dfpre  38721  fourierdlem89  46547  fourierdlem90  46548  fourierdlem91  46549  fourierdlem96  46554  fourierdlem97  46555  fourierdlem98  46556  fourierdlem99  46557  fourierdlem100  46558  fourierdlem112  46570