Theorem iotabii 6324

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

Syntax hints:   ↔ wb 209   = wceq 1542  ℩cio 6295

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-in 3850  df-ss 3860  df-uni 4797  df-iota 6297

This theorem is referenced by:  riotav  7132  ovtpos  7936  cbvsum  15145  cbvprod  15361  oppgid  18602  oppr1  19506  riotarab  33246  fourierdlem89  43278  fourierdlem90  43279  fourierdlem91  43280  fourierdlem96  43285  fourierdlem97  43286  fourierdlem98  43287  fourierdlem99  43288  fourierdlem100  43289  fourierdlem112  43301