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

Theorem riota2 6070
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 2574 . 2  |-  F/_ x B
2 nfv 1673 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6069 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 1369    e. wcel 1756   E!wreu 2712   iota_crio 6046
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-rex 2716  df-reu 2717  df-v 2969  df-sbc 3182  df-un 3328  df-sn 3873  df-pr 3875  df-uni 4087  df-iota 5376  df-riota 6047
This theorem is referenced by:  eqsup  7698  fin23lem22  8488  subadd  9605  divmul  9989  uzinfmi  10926  fllelt  11639  flval2  11654  flbi  11656  remim  12598  resqrcl  12735  resqrthlem  12736  sqrneg  12749  sqrthlem  12842  divalgmod  13602  qnumdenbi  13814  catidd  14610  lubprop  15148  glbprop  15161  isglbd  15279  poslubd  15310  ismgmid  15427  isgrpinv  15579  pj1id  16187  coeeq  21670  ismir  23031  mireq  23035  usgraidx2vlem2  23261  nbgraf1olem3  23303  cmpidelt  23767  cnid  23789  addinv  23790  mulid  23794  hilid  24514  pjpreeq  24752  cnvbraval  25465  cdj3lem2  25790  xdivmul  26051  cvmliftphtlem  27158  cvmlift3lem4  27163  cvmlift3lem6  27165  cvmlift3lem9  27168  transportprops  28016  ltflcei  28372  lxflflp1  28374  exidresid  28697  frgrancvvdeqlem4  30579  lshpkrlem1  32595  cdlemeiota  34069  dochfl1  34961  hgmapvs  35379
  Copyright terms: Public domain W3C validator