Theorem riota5 7436

Description: A method for computing restricted iota. (Contributed by NM, 20-Oct-2011.) (Revised by Mario Carneiro, 6-Dec-2016.)

Hypotheses

Ref	Expression
riota5.1	⊢ (𝜑 → 𝐵 ∈ 𝐴)
riota5.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))

Assertion

Ref	Expression
riota5	⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem riota5

Step	Hyp	Ref	Expression
1		nfcvd 2909	. 2 ⊢ (𝜑 → Ⅎ𝑥𝐵)
2		riota5.1	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
3		riota5.2	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))
4	1, 2, 3	riota5f 7435	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ℩crio 7405

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-reu 3389  df-v 3490  df-sbc 3805  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6527  df-riota 7406

This theorem is referenced by:  f1ocnvfv3  7445  ttrcltr  9787  sqrt0  15292  lubid  18434  lubun  18587  odval2  19595  adjvalval  31971  xdivpnfrp  32899  xrsinvgval  32993  dfgcd3  37292  poimirlem6  37588  poimirlem7  37589  lub0N  39147  glb0N  39151  trlval2  40122  cdlemefrs32fva  40359  cdleme32fva  40396  cdlemg1a  40529  unxpwdom3  43054