Theorem iotabii 6528

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

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

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 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-uni 4878  df-iota 6499

This theorem is used by:  riotav  7385  riotarab  7422  ovtpos  8246  cbvsum  15772  cbvsumv  15773  cbvprod  15993  cbvprodv  15994  prodeq1i  15996  oppgid  19457  oppr1  20465  riotaeqbii  36751  sumeq2si  36755  prodeq2si  36757  cbvprodvw2  36800  dfpre  39166  fourierdlem89  46950  fourierdlem90  46951  fourierdlem91  46952  fourierdlem96  46957  fourierdlem97  46958  fourierdlem98  46959  fourierdlem99  46960  fourierdlem100  46961  fourierdlem112  46973