Theorem riota5 7380

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ℩crio 7350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2880  df-ral 3047  df-rex 3056  df-reu 3358  df-v 3457  df-sbc 3762  df-un 3927  df-ss 3939  df-sn 4598  df-pr 4600  df-uni 4880  df-iota 6472  df-riota 7351

This theorem is referenced by:  f1ocnvfv3  7389  ttrcltr  9687  sqrt0  15217  lubid  18327  lubun  18480  odval2  19487  adjvalval  31873  xdivpnfrp  32861  xrsinvgval  32954  dfgcd3  37309  poimirlem6  37617  poimirlem7  37618  lub0N  39174  glb0N  39178  trlval2  40149  cdlemefrs32fva  40386  cdleme32fva  40423  cdlemg1a  40556  unxpwdom3  43056