Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > iotabidv | Structured version Visualization version GIF version |
Description: Formula-building deduction rule 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 1842 | . 2 ⊢ (𝜑 → ∀𝑥(𝜓 ↔ 𝜒)) |
3 | iotabi 5777 | . 2 ⊢ (∀𝑥(𝜓 ↔ 𝜒) → (℩𝑥𝜓) = (℩𝑥𝜒)) | |
4 | 2, 3 | syl 17 | 1 ⊢ (𝜑 → (℩𝑥𝜓) = (℩𝑥𝜒)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∀wal 1473 = wceq 1475 ℩cio 5766 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rex 2902 df-uni 4373 df-iota 5768 |
This theorem is referenced by: csbiota 5797 dffv3 6099 fveq1 6102 fveq2 6103 fvres 6117 csbfv12 6141 opabiota 6171 fvco2 6183 fvopab5 6217 riotaeqdv 6512 riotabidv 6513 riotabidva 6527 erov 7731 iunfictbso 8820 isf32lem9 9066 shftval 13662 sumeq1 14267 sumeq2w 14270 sumeq2ii 14271 zsum 14296 isumclim3 14332 isumshft 14410 prodeq1f 14477 prodeq2w 14481 prodeq2ii 14482 zprod 14506 iprodclim3 14570 pcval 15387 grpidval 17083 grpidpropd 17084 gsumvalx 17093 gsumpropd 17095 gsumpropd2lem 17096 gsumress 17099 psgnfval 17743 psgnval 17750 psgndif 19767 dchrptlem1 24789 lgsdchrval 24879 ajval 27101 adjval 28133 resv1r 29168 bj-finsumval0 32324 uncov 32560 |
Copyright terms: Public domain | W3C validator |