Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  riota5 Structured version   Visualization version   GIF version

Theorem riota5 6536
 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
StepHypRef Expression
1 nfcvd 2752 . 2 (𝜑𝑥𝐵)
2 riota5.1 . 2 (𝜑𝐵𝐴)
3 riota5.2 . 2 ((𝜑𝑥𝐴) → (𝜓𝑥 = 𝐵))
41, 2, 3riota5f 6535 1 (𝜑 → (𝑥𝐴 𝜓) = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ℩crio 6510 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-reu 2903  df-v 3175  df-sbc 3403  df-un 3545  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-riota 6511 This theorem is referenced by:  f1ocnvfv3  6545  sqrt0  13830  lubid  16813  lubun  16946  odval2  17793  adjvalval  28180  xdivpnfrp  28972  xrsinvgval  29008  poimirlem6  32585  poimirlem7  32586  lub0N  33494  glb0N  33498  trlval2  34468  cdlemefrs32fva  34706  cdleme32fva  34743  cdlemg1a  34876  unxpwdom3  36683
 Copyright terms: Public domain W3C validator