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 6405 | . 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (℩𝑥𝜑) = (℩𝑥𝜓)) | |
2 | iotabii.1 | . 2 ⊢ (𝜑 ↔ 𝜓) | |
3 | 1, 2 | mpg 1800 | 1 ⊢ (℩𝑥𝜑) = (℩𝑥𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1539 ℩cio 6389 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-in 3894 df-ss 3904 df-uni 4840 df-iota 6391 |
This theorem is referenced by: riotav 7237 ovtpos 8057 cbvsum 15407 cbvprod 15625 oppgid 18963 oppr1 19876 riotarab 33673 fourierdlem89 43736 fourierdlem90 43737 fourierdlem91 43738 fourierdlem96 43743 fourierdlem97 43744 fourierdlem98 43745 fourierdlem99 43746 fourierdlem100 43747 fourierdlem112 43759 |
Copyright terms: Public domain | W3C validator |