Theorem riota5 7346

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ral 3056  df-rex 3066  df-reu 3347  df-v 3435  df-sbc 3726  df-un 3890  df-ss 3902  df-sn 4559  df-pr 4561  df-uni 4842  df-iota 6445  df-riota 7317

This theorem is referenced by:  f1ocnvfv3  7355  ttrcltr  9632  sqrt0  15198  lubid  18321  lubun  18476  odval2  19521  adjvalval  32030  xdivpnfrp  33015  xrsinvgval  33091  dfgcd3  37699  poimirlem6  38008  poimirlem7  38009  lub0N  39696  glb0N  39700  trlval2  40670  cdlemefrs32fva  40907  cdleme32fva  40944  cdlemg1a  41077  unxpwdom3  43555