![]() |
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 1903 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
3 | iotabi 6190 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∀wal 1518 = wceq 1520 ℩cio 6179 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-5 1886 ax-6 1945 ax-7 1990 ax-8 2081 ax-9 2089 ax-ext 2767 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1760 df-sb 2041 df-clab 2774 df-cleq 2786 df-clel 2861 df-rex 3109 df-uni 4740 df-iota 6181 |
This theorem is referenced by: csbiota 6210 dffv3 6526 fveq1 6529 fveq2 6530 fvres 6549 csbfv12 6573 opabiota 6605 fvco2 6617 fvopab5 6656 riotaeqdv 6969 riotabidv 6970 riotabidva 6984 erov 8235 iunfictbso 9375 isf32lem9 9618 shftval 14255 sumeq1 14867 sumeq2w 14870 sumeq2ii 14871 zsum 14896 isumclim3 14935 isumshft 15015 prodeq1f 15083 prodeq2w 15087 prodeq2ii 15088 zprod 15112 iprodclim3 15175 pcval 15998 grpidval 17687 grpidpropd 17688 gsumvalx 17697 gsumpropd 17699 gsumpropd2lem 17700 gsumress 17703 psgnfval 18347 psgnval 18354 psgndif 20416 dchrptlem1 25510 lgsdchrval 25600 ajval 28317 adjval 29346 resv1r 30519 nosupfv 32760 noeta 32776 bj-finsumval0 34065 uncov 34350 afv2eq12d 42884 funressndmafv2rn 42892 afv2res 42908 dfafv23 42922 afv2co2 42926 |
Copyright terms: Public domain | W3C validator |