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

Theorem riota5 6179
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 2614 . 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 6178 1  |-  ( ph  ->  ( iota_ x  e.  A  ps )  =  B
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1370    e. wcel 1758   iota_crio 6152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ral 2800  df-rex 2801  df-reu 2802  df-v 3072  df-sbc 3287  df-un 3433  df-sn 3978  df-pr 3980  df-uni 4192  df-iota 5481  df-riota 6153
This theorem is referenced by:  f1ocnvfv3  6188  sqr0  12835  lubid  15264  lubun  15397  odval2  16160  adjvalval  25478  xdivpnfrp  26244  xrsinvgval  26274  unxpwdom3  29588  lub0N  33142  glb0N  33146  trlval2  34115  cdlemefrs32fva  34352  cdleme32fva  34389  cdlemg1a  34522
  Copyright terms: Public domain W3C validator