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

Theorem riota2 6266
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 2629 . 2  |-  F/_ x B
2 nfv 1683 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6265 1  |-  ( ( B  e.  A  /\  E! x  e.  A  ph )  ->  ( ps  <->  (
iota_ x  e.  A  ph )  =  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379    e. wcel 1767   E!wreu 2816   iota_crio 6242
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-reu 2821  df-v 3115  df-sbc 3332  df-un 3481  df-sn 4028  df-pr 4030  df-uni 4246  df-iota 5549  df-riota 6243
This theorem is referenced by:  eqsup  7912  fin23lem22  8703  subadd  9819  divmul  10206  uzinfmi  11157  fllelt  11898  flflp1  11908  flval2  11914  flbi  11916  remim  12909  resqrtcl  13046  resqrtthlem  13047  sqrtneg  13060  sqrtthlem  13154  divalgmod  13919  qnumdenbi  14132  catidd  14931  lubprop  15469  glbprop  15482  isglbd  15600  poslubd  15631  ismgmid  15748  isgrpinv  15901  pj1id  16513  coeeq  22359  ismir  23753  mireq  23759  ismidb  23821  islmib  23830  usgraidx2vlem2  24068  nbgraf1olem3  24119  frgrancvvdeqlem4  24710  cmpidelt  25007  cnid  25029  addinv  25030  mulid  25034  hilid  25754  pjpreeq  25992  cnvbraval  26705  cdj3lem2  27030  xdivmul  27289  cvmliftphtlem  28402  cvmlift3lem4  28407  cvmlift3lem6  28409  cvmlift3lem9  28412  transportprops  29261  ltflcei  29620  exidresid  29944  fourierdlem50  31457  usgedgvadf1lem2  31883  usgedgvadf1ALTlem2  31886  lshpkrlem1  33907  cdlemeiota  35381  dochfl1  36273  hgmapvs  36691
  Copyright terms: Public domain W3C validator