|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > iotabii | Structured version Visualization version GIF version | ||
| Description: Formula-building deduction for iota. (Contributed by Mario Carneiro, 2-Oct-2015.) | 
| Ref | Expression | 
|---|---|
| iotabii.1 | ⊢ (𝜑 ↔ 𝜓) | 
| Ref | Expression | 
|---|---|
| iotabii | ⊢ (℩𝑥𝜑) = (℩𝑥𝜓) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | iotabi 6526 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓)) | |
| 2 | iotabii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
| 3 | 1, 2 | mpg 1796 | 1 ⊢ (℩𝑥𝜑) = (℩𝑥𝜓) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 = wceq 1539 ℩cio 6511 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-ss 3967 df-uni 4907 df-iota 6513 | 
| This theorem is referenced by: riotav 7394 riotarab 7431 ovtpos 8267 cbvsum 15732 cbvsumv 15733 cbvprod 15950 cbvprodv 15951 prodeq1i 15953 oppgid 19376 oppr1 20351 riotaeqbii 36200 sumeq2si 36204 prodeq2si 36206 cbvprodvw2 36249 fourierdlem89 46215 fourierdlem90 46216 fourierdlem91 46217 fourierdlem96 46222 fourierdlem97 46223 fourierdlem98 46224 fourierdlem99 46225 fourierdlem100 46226 fourierdlem112 46238 | 
| Copyright terms: Public domain | W3C validator |