![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > riota5 | Structured version Visualization version GIF version |
Description: A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.) |
Ref | Expression |
---|---|
riota5.1 | ⊢ (𝜑 → 𝐵 ∈ 𝐴) |
riota5.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵)) |
Ref | Expression |
---|---|
riota5 | ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcvd 2969 | . 2 ⊢ (𝜑 → Ⅎ𝑥𝐵) | |
2 | riota5.1 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝐴) | |
3 | riota5.2 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵)) | |
4 | 1, 2, 3 | riota5f 6890 | 1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1658 ∈ wcel 2166 ℩crio 6864 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1896 ax-4 1910 ax-5 2011 ax-6 2077 ax-7 2114 ax-9 2175 ax-10 2194 ax-11 2209 ax-12 2222 ax-13 2390 ax-ext 2802 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 881 df-3an 1115 df-tru 1662 df-ex 1881 df-nf 1885 df-sb 2070 df-mo 2604 df-eu 2639 df-clab 2811 df-cleq 2817 df-clel 2820 df-nfc 2957 df-ral 3121 df-rex 3122 df-reu 3123 df-v 3415 df-sbc 3662 df-un 3802 df-sn 4397 df-pr 4399 df-uni 4658 df-iota 6085 df-riota 6865 |
This theorem is referenced by: f1ocnvfv3 6900 sqrt0 14358 lubid 17342 lubun 17475 odval2 18320 adjvalval 29350 xdivpnfrp 30185 xrsinvgval 30221 dfgcd3 33715 poimirlem6 33958 poimirlem7 33959 lub0N 35263 glb0N 35267 trlval2 36237 cdlemefrs32fva 36474 cdleme32fva 36511 cdlemg1a 36644 unxpwdom3 38507 |
Copyright terms: Public domain | W3C validator |