Theorem iotabii 6477

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

Syntax hints:   ↔ wb 207   = wceq 1547  ℩cio 6446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-uni 4846  df-iota 6448

This theorem is referenced by:  riotav  7325  riotarab  7362  ovtpos  8188  cbvsum  15655  cbvsumv  15656  cbvprod  15876  cbvprodv  15877  prodeq1i  15879  oppgid  19329  oppr1  20328  riotaeqbii  36433  sumeq2si  36437  prodeq2si  36439  cbvprodvw2  36482  dfpre  38850  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem96  46652  fourierdlem97  46653  fourierdlem98  46654  fourierdlem99  46655  fourierdlem100  46656  fourierdlem112  46668