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

Theorem riota2 6289
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 2580 . 2  |-  F/_ x B
2 nfv 1755 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6288 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 187    /\ wa 370    = wceq 1437    e. wcel 1872   E!wreu 2773   iota_crio 6266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ral 2776  df-rex 2777  df-reu 2778  df-v 3082  df-sbc 3300  df-un 3441  df-sn 3999  df-pr 4001  df-uni 4220  df-iota 5565  df-riota 6267
This theorem is referenced by:  eqsup  7979  sup0  7989  fin23lem22  8764  subadd  9885  divmul  10280  uzinfmiOLD  11246  fllelt  12039  flflp1  12049  flval2  12055  flbi  12057  remim  13180  resqrtcl  13317  resqrtthlem  13318  sqrtneg  13331  sqrtthlem  13425  divalgmod  14386  qnumdenbi  14692  catidd  15585  lubprop  16231  glbprop  16244  isglbd  16362  poslubd  16393  ismgmid  16506  isgrpinv  16715  pj1id  17348  coeeq  23179  ismir  24702  mireq  24708  ismidb  24818  islmib  24827  usgraidx2vlem2  25117  nbgraf1olem3  25169  frgrancvvdeqlem4  25759  cmpidelt  26055  cnid  26077  addinv  26078  mulid  26082  hilid  26812  pjpreeq  27049  cnvbraval  27761  cdj3lem2  28086  xdivmul  28401  cvmliftphtlem  30048  cvmlift3lem4  30053  cvmlift3lem6  30055  cvmlift3lem9  30058  transportprops  30806  ltflcei  31897  exidresid  32141  lshpkrlem1  32645  cdlemeiota  34121  dochfl1  35013  hgmapvs  35431  wessf1ornlem  37420  fourierdlem50  37960  usgridx2vlem2  39087  usgedgvadf1lem2  39346  usgedgvadf1ALTlem2  39349
  Copyright terms: Public domain W3C validator