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

Theorem riota2 6327
Description: This theorem shows a condition that allows us to represent a descriptor with a class expression  B. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)
Hypothesis
Ref Expression
riota2.1  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
riota2  |-  ( ( B  e.  A  /\  E! x  e.  A  ph )  ->  ( ps  <->  (
iota_ x  e.  A ph )  =  B
) )
Distinct variable groups:    ps, x    x, A    x, B
Allowed substitution hint:    ph( x)

Proof of Theorem riota2
StepHypRef Expression
1 nfcv 2419 . 2  |-  F/_ x B
2 nfv 1605 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6326 1  |-  ( ( B  e.  A  /\  E! x  e.  A  ph )  ->  ( ps  <->  (
iota_ x  e.  A ph )  =  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623    e. wcel 1684   E!wreu 2545   iota_crio 6297
This theorem is referenced by:  eqsup  7207  fin23lem22  7953  subadd  9054  divmul  9427  lbinfm  9707  uzinfmi  10297  fllelt  10929  flval2  10944  flbi  10946  remim  11602  resqrcl  11739  resqrthlem  11740  sqrneg  11753  sqrthlem  11846  divalgmod  12605  qnumdenbi  12815  catidd  13582  lubprop  14114  glbprop  14119  isglbd  14221  poslubd  14251  spwpr4  14340  ismgmid  14387  isgrpinv  14532  pj1id  15008  coeeq  19609  cmpidelt  20996  cnid  21018  addinv  21019  mulid  21023  hilid  21740  pjpreeq  21977  cnvbraval  22690  cdj3lem2  23015  xdivmul  23108  cvmliftphtlem  23848  cvmlift3lem4  23853  cvmlift3lem6  23855  cvmlift3lem9  23858  transportprops  24657  subaddv  25671  lineval42  26080  exidresid  26569  lshpkrlem1  29300  cdlemeiota  30774  dochfl1  31666  hgmapvs  32084
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-reu 2550  df-v 2790  df-sbc 2992  df-un 3157  df-if 3566  df-sn 3646  df-pr 3647  df-uni 3828  df-iota 5219  df-riota 6304
  Copyright terms: Public domain W3C validator