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

Theorem riota2 6343
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 2432 . 2  |-  F/_ x B
2 nfv 1609 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6342 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 1632    e. wcel 1696   E!wreu 2558   iota_crio 6313
This theorem is referenced by:  eqsup  7223  fin23lem22  7969  subadd  9070  divmul  9443  lbinfm  9723  uzinfmi  10313  fllelt  10945  flval2  10960  flbi  10962  remim  11618  resqrcl  11755  resqrthlem  11756  sqrneg  11769  sqrthlem  11862  divalgmod  12621  qnumdenbi  12831  catidd  13598  lubprop  14130  glbprop  14135  isglbd  14237  poslubd  14267  spwpr4  14356  ismgmid  14403  isgrpinv  14548  pj1id  15024  coeeq  19625  cmpidelt  21012  cnid  21034  addinv  21035  mulid  21039  hilid  21756  pjpreeq  21993  cnvbraval  22706  cdj3lem2  23031  xdivmul  23124  cvmliftphtlem  23863  cvmlift3lem4  23868  cvmlift3lem6  23870  cvmlift3lem9  23873  transportprops  24729  ltflcei  24998  lxflflp1  25000  subaddv  25774  lineval42  26183  exidresid  26672  lshpkrlem1  29922  cdlemeiota  31396  dochfl1  32288  hgmapvs  32706
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-reu 2563  df-v 2803  df-sbc 3005  df-un 3170  df-if 3579  df-sn 3659  df-pr 3660  df-uni 3844  df-iota 5235  df-riota 6320
  Copyright terms: Public domain W3C validator