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

Theorem riota5 6891
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 2969 . 2 (𝜑𝑥𝐵)
2 riota5.1 . 2 (𝜑𝐵𝐴)
3 riota5.2 . 2 ((𝜑𝑥𝐴) → (𝜓𝑥 = 𝐵))
41, 2, 3riota5f 6890 1 (𝜑 → (𝑥𝐴 𝜓) = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386   = wceq 1658  wcel 2166  crio 6864
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ral 3121  df-rex 3122  df-reu 3123  df-v 3415  df-sbc 3662  df-un 3802  df-sn 4397  df-pr 4399  df-uni 4658  df-iota 6085  df-riota 6865
This theorem is referenced by:  f1ocnvfv3  6900  sqrt0  14358  lubid  17342  lubun  17475  odval2  18320  adjvalval  29350  xdivpnfrp  30185  xrsinvgval  30221  dfgcd3  33715  poimirlem6  33958  poimirlem7  33959  lub0N  35263  glb0N  35267  trlval2  36237  cdlemefrs32fva  36474  cdleme32fva  36511  cdlemg1a  36644  unxpwdom3  38507
  Copyright terms: Public domain W3C validator