Theorem iotabii 6502

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

Syntax hints:   ↔ wb 208   = wceq 1559  ℩cio 6471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-ss 3921  df-uni 4865  df-iota 6473

This theorem is referenced by:  riotav  7354  riotarab  7391  ovtpos  8216  cbvsum  15705  cbvsumv  15706  cbvprod  15926  cbvprodv  15927  prodeq1i  15929  oppgid  19379  oppr1  20378  riotaeqbii  36522  sumeq2si  36526  prodeq2si  36528  cbvprodvw2  36571  dfpre  38939  fourierdlem89  46733  fourierdlem90  46734  fourierdlem91  46735  fourierdlem96  46740  fourierdlem97  46741  fourierdlem98  46742  fourierdlem99  46743  fourierdlem100  46744  fourierdlem112  46756