| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > iotabidv | Structured version Visualization version GIF version | ||
| Description: Formula-building deduction for iota. (Contributed by NM, 20-Aug-2011.) |
| Ref | Expression |
|---|---|
| iotabidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
| Ref | Expression |
|---|---|
| iotabidv | ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iotabidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | alrimiv 1927 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
| 3 | iotabi 6527 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒)) | |
| 4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 = wceq 1540 ℩cio 6512 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-ss 3968 df-uni 4908 df-iota 6514 |
| This theorem is referenced by: csbiota 6554 dffv3 6902 fveq1 6905 fveq2 6906 fvres 6925 csbfv12 6954 opabiota 6991 fvco2 7006 fvopab5 7049 riotaeqdv 7389 riotabidv 7390 riotabidva 7407 erov 8854 iunfictbso 10154 isf32lem9 10401 shftval 15113 sumeq1 15725 sumeq2w 15728 sumeq2ii 15729 sumeq2sdv 15739 zsum 15754 isumclim3 15795 isumshft 15875 prodeq1f 15942 prodeq1 15943 prodeq2w 15946 prodeq2ii 15947 prodeq2sdv 15959 zprod 15973 iprodclim3 16036 pcval 16882 grpidval 18674 grpidpropd 18675 gsumvalx 18689 gsumpropd 18691 gsumpropd2lem 18692 gsumress 18695 psgnfval 19518 psgnval 19525 psgndif 21620 dchrptlem1 27308 lgsdchrval 27398 nosupcbv 27747 nosupfv 27751 noinfcbv 27762 noinffv 27766 ajval 30880 adjval 31909 urpropd 33236 resv1r 33368 opprqus0g 33518 prodeq12sdv 36219 cbvsumdavw 36280 cbvproddavw 36281 cbvsumdavw2 36296 cbvproddavw2 36297 bj-finsumval0 37286 uncov 37608 afv2eq12d 47227 funressndmafv2rn 47235 afv2res 47251 dfafv23 47265 afv2co2 47269 |
| Copyright terms: Public domain | W3C validator |