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

Theorem riota2 6198
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 2554 . 2  |-  F/_ x B
2 nfv 1722 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6197 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 367    = wceq 1399    e. wcel 1836   E!wreu 2744   iota_crio 6175
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2016  ax-ext 2370
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2232  df-clab 2378  df-cleq 2384  df-clel 2387  df-nfc 2542  df-ral 2747  df-rex 2748  df-reu 2749  df-v 3049  df-sbc 3266  df-un 3407  df-sn 3958  df-pr 3960  df-uni 4177  df-iota 5473  df-riota 6176
This theorem is referenced by:  eqsup  7848  fin23lem22  8638  subadd  9754  divmul  10145  uzinfmi  11098  fllelt  11852  flflp1  11862  flval2  11868  flbi  11870  remim  12971  resqrtcl  13108  resqrtthlem  13109  sqrtneg  13122  sqrtthlem  13216  divalgmod  14085  qnumdenbi  14298  catidd  15106  lubprop  15752  glbprop  15765  isglbd  15883  poslubd  15914  ismgmid  16027  isgrpinv  16236  pj1id  16853  coeeq  22728  ismir  24181  mireq  24187  ismidb  24285  islmib  24294  usgraidx2vlem2  24534  nbgraf1olem3  24585  frgrancvvdeqlem4  25175  cmpidelt  25469  cnid  25491  addinv  25492  mulid  25496  hilid  26216  pjpreeq  26454  cnvbraval  27166  cdj3lem2  27491  xdivmul  27804  cvmliftphtlem  28987  cvmlift3lem4  28992  cvmlift3lem6  28994  cvmlift3lem9  28997  transportprops  29873  ltflcei  30244  exidresid  30543  fourierdlem50  32140  usgedgvadf1lem2  32767  usgedgvadf1ALTlem2  32770  lshpkrlem1  35283  cdlemeiota  36759  dochfl1  37651  hgmapvs  38069
  Copyright terms: Public domain W3C validator