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

Theorem riota2 6304
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 2603 . 2  |-  F/_ x B
2 nfv 1772 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6303 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 189    /\ wa 375    = wceq 1455    e. wcel 1898   E!wreu 2751   iota_crio 6281
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-reu 2756  df-v 3059  df-sbc 3280  df-un 3421  df-sn 3981  df-pr 3983  df-uni 4213  df-iota 5569  df-riota 6282
This theorem is referenced by:  eqsup  8001  sup0  8011  fin23lem22  8788  subadd  9909  divmul  10306  uzinfmiOLD  11273  fllelt  12071  flflp1  12081  flval2  12087  flbi  12089  remim  13235  resqrtcl  13372  resqrtthlem  13373  sqrtneg  13386  sqrtthlem  13480  divalgmod  14442  qnumdenbi  14748  catidd  15641  lubprop  16287  glbprop  16300  isglbd  16418  poslubd  16449  ismgmid  16562  isgrpinv  16771  pj1id  17404  coeeq  23237  ismir  24760  mireq  24766  ismidb  24876  islmib  24885  usgraidx2vlem2  25175  nbgraf1olem3  25227  frgrancvvdeqlem4  25817  cmpidelt  26113  cnid  26135  addinv  26136  mulid  26140  hilid  26870  pjpreeq  27107  cnvbraval  27819  cdj3lem2  28144  xdivmul  28446  cvmliftphtlem  30090  cvmlift3lem4  30095  cvmlift3lem6  30097  cvmlift3lem9  30100  transportprops  30851  ltflcei  31979  exidresid  32223  lshpkrlem1  32722  cdlemeiota  34198  dochfl1  35090  hgmapvs  35508  wessf1ornlem  37513  fourierdlem50  38121  usgredg2vlem2  39449  usgedgvadf1lem2  40095  usgedgvadf1ALTlem2  40098
  Copyright terms: Public domain W3C validator