Theorem iotabii 6523

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ℩cio 6492

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-uni 4867  df-iota 6494

This theorem is used by:  riotav  7382  riotarab  7419  ovtpos  8261  cbvsum  15867  cbvsumv  15868  cbvprod  16087  cbvprodv  16088  prodeq1i  16090  oppgid  19575  oppr1  20585  riotaeqbii  37079  sumeq2si  37083  prodeq2si  37085  cbvprodvw2  37128  dfpre  39501  fourierdlem89  47298  fourierdlem90  47299  fourierdlem91  47300  fourierdlem96  47305  fourierdlem97  47306  fourierdlem98  47307  fourierdlem99  47308  fourierdlem100  47309  fourierdlem112  47321