Theorem iotabii 6522

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

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

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 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-uni 4871  df-iota 6493

This theorem is used by:  riotav  7379  riotarab  7416  ovtpos  8243  cbvsum  15786  cbvsumv  15787  cbvprod  16006  cbvprodv  16007  prodeq1i  16009  oppgid  19489  oppr1  20497  riotaeqbii  36826  sumeq2si  36830  prodeq2si  36832  cbvprodvw2  36875  dfpre  39232  fourierdlem89  47031  fourierdlem90  47032  fourierdlem91  47033  fourierdlem96  47038  fourierdlem97  47039  fourierdlem98  47040  fourierdlem99  47041  fourierdlem100  47042  fourierdlem112  47054