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

Theorem riota5 6221
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  |-  ( ph  ->  B  e.  A )
riota5.2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  x  =  B ) )
Assertion
Ref Expression
riota5  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  B
)
Distinct variable groups:    x, A    x, B    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem riota5
StepHypRef Expression
1 nfcvd 2565 . 2  |-  ( ph  -> 
F/_ x B )
2 riota5.1 . 2  |-  ( ph  ->  B  e.  A )
3 riota5.2 . 2  |-  ( (
ph  /\  x  e.  A )  ->  ( ps 
<->  x  =  B ) )
41, 2, 3riota5f 6220 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 367    = wceq 1405    e. wcel 1842   iota_crio 6195
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-rex 2759  df-reu 2760  df-v 3060  df-sbc 3277  df-un 3418  df-sn 3972  df-pr 3974  df-uni 4191  df-iota 5489  df-riota 6196
This theorem is referenced by:  f1ocnvfv3  6230  sqrt0  13131  lubid  15836  lubun  15969  odval2  16791  adjvalval  27149  xdivpnfrp  27961  xrsinvgval  27997  lub0N  32188  glb0N  32192  trlval2  33162  cdlemefrs32fva  33400  cdleme32fva  33437  cdlemg1a  33570  unxpwdom3  35384
  Copyright terms: Public domain W3C validator