Theorem iotabii 6516

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570  ℩cio 6485

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-uni 4868  df-iota 6487

This theorem is used by:  riotav  7374  riotarab  7411  ovtpos  8242  cbvsum  15842  cbvsumv  15843  cbvprod  16062  cbvprodv  16063  prodeq1i  16065  oppgid  19550  oppr1  20560  riotaeqbii  36957  sumeq2si  36961  prodeq2si  36963  cbvprodvw2  37006  dfpre  39376  fourierdlem89  47149  fourierdlem90  47150  fourierdlem91  47151  fourierdlem96  47156  fourierdlem97  47157  fourierdlem98  47158  fourierdlem99  47159  fourierdlem100  47160  fourierdlem112  47172