Theorem iotabii 6545

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-uni 4871  df-iota 6515

This theorem is used by:  riotav  7408  riotarab  7445  ovtpos  8289  cbvsum  15894  cbvsumv  15895  cbvprod  16114  cbvprodv  16115  prodeq1i  16117  oppgid  19603  oppr1  20613  riotaeqbii  37178  sumeq2si  37182  prodeq2si  37184  cbvprodvw2  37227  dfpre  39611  fourierdlem89  47420  fourierdlem90  47421  fourierdlem91  47422  fourierdlem96  47427  fourierdlem97  47428  fourierdlem98  47429  fourierdlem99  47430  fourierdlem100  47431  fourierdlem112  47443