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

Theorem riota2 6531
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 2540 . 2  |-  F/_ x B
2 nfv 1626 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6530 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 177    /\ wa 359    = wceq 1649    e. wcel 1721   E!wreu 2668   iota_crio 6501
This theorem is referenced by:  eqsup  7417  fin23lem22  8163  subadd  9264  divmul  9637  uzinfmi  10511  fllelt  11161  flval2  11176  flbi  11178  remim  11877  resqrcl  12014  resqrthlem  12015  sqrneg  12028  sqrthlem  12121  divalgmod  12881  qnumdenbi  13091  catidd  13860  lubprop  14392  glbprop  14397  isglbd  14499  poslubd  14529  spwpr4  14618  ismgmid  14665  isgrpinv  14810  pj1id  15286  coeeq  20099  usgraidx2vlem2  21364  nbgraf1olem3  21406  cmpidelt  21870  cnid  21892  addinv  21893  mulid  21897  hilid  22616  pjpreeq  22853  cnvbraval  23566  cdj3lem2  23891  xdivmul  24124  cvmliftphtlem  24957  cvmlift3lem4  24962  cvmlift3lem6  24964  cvmlift3lem9  24967  transportprops  25872  ltflcei  26140  lxflflp1  26142  exidresid  26444  frgrancvvdeqlem4  28136  lshpkrlem1  29593  cdlemeiota  31067  dochfl1  31959  hgmapvs  32377
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-rex 2672  df-reu 2673  df-v 2918  df-sbc 3122  df-un 3285  df-if 3700  df-sn 3780  df-pr 3781  df-uni 3976  df-iota 5377  df-riota 6508
  Copyright terms: Public domain W3C validator