Theorem riota5 7421

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 2905	. 2 ⊢ (𝜑 → Ⅎ𝑥𝐵)
2		riota5.1	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
3		riota5.2	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝑥 = 𝐵))
4	1, 2, 3	riota5f 7420	1 ⊢ (𝜑 → (℩𝑥 ∈ 𝐴 𝜓) = 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1538   ∈ wcel 2107  ℩crio 7391

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 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1541  df-ex 1778  df-nf 1782  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ral 3061  df-rex 3070  df-reu 3380  df-v 3481  df-sbc 3793  df-un 3969  df-ss 3981  df-sn 4633  df-pr 4635  df-uni 4914  df-iota 6519  df-riota 7392

This theorem is referenced by:  f1ocnvfv3  7430  ttrcltr  9760  sqrt0  15283  lubid  18426  lubun  18579  odval2  19590  adjvalval  31979  xdivpnfrp  32913  xrsinvgval  33006  dfgcd3  37319  poimirlem6  37625  poimirlem7  37626  lub0N  39183  glb0N  39187  trlval2  40158  cdlemefrs32fva  40395  cdleme32fva  40432  cdlemg1a  40565  unxpwdom3  43098