Theorem iotabii 6471

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

Syntax hints:   ↔ wb 206   = wceq 1540  ℩cio 6440

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-uni 4862  df-iota 6442

This theorem is referenced by:  riotav  7315  riotarab  7352  ovtpos  8181  cbvsum  15620  cbvsumv  15621  cbvprod  15838  cbvprodv  15839  prodeq1i  15841  oppgid  19253  oppr1  20253  riotaeqbii  36171  sumeq2si  36175  prodeq2si  36177  cbvprodvw2  36220  fourierdlem89  46177  fourierdlem90  46178  fourierdlem91  46179  fourierdlem96  46184  fourierdlem97  46185  fourierdlem98  46186  fourierdlem99  46187  fourierdlem100  46188  fourierdlem112  46200