Theorem iotabii 6510

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

Syntax hints:   ↔ wb 209   = wceq 1563  ℩cio 6479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-uni 4869  df-iota 6481

This theorem is referenced by:  riotav  7362  riotarab  7399  ovtpos  8225  cbvsum  15736  cbvsumv  15737  cbvprod  15957  cbvprodv  15958  prodeq1i  15960  oppgid  19417  oppr1  20423  riotaeqbii  36571  sumeq2si  36575  prodeq2si  36577  cbvprodvw2  36620  dfpre  38987  fourierdlem89  46767  fourierdlem90  46768  fourierdlem91  46769  fourierdlem96  46774  fourierdlem97  46775  fourierdlem98  46776  fourierdlem99  46777  fourierdlem100  46778  fourierdlem112  46790