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

Theorem riota2 6262
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 1692 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6261 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 1381    e. wcel 1802   E!wreu 2793   iota_crio 6238
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ral 2796  df-rex 2797  df-reu 2798  df-v 3095  df-sbc 3312  df-un 3464  df-sn 4012  df-pr 4014  df-uni 4232  df-iota 5538  df-riota 6239
This theorem is referenced by:  eqsup  7915  fin23lem22  8707  subadd  9825  divmul  10213  uzinfmi  11167  fllelt  11910  flflp1  11920  flval2  11926  flbi  11928  remim  12926  resqrtcl  13063  resqrtthlem  13064  sqrtneg  13077  sqrtthlem  13171  divalgmod  13938  qnumdenbi  14151  catidd  14951  lubprop  15487  glbprop  15500  isglbd  15618  poslubd  15649  ismgmid  15762  isgrpinv  15971  pj1id  16588  coeeq  22494  ismir  23909  mireq  23915  ismidb  24013  islmib  24022  usgraidx2vlem2  24261  nbgraf1olem3  24312  frgrancvvdeqlem4  24902  cmpidelt  25200  cnid  25222  addinv  25223  mulid  25227  hilid  25947  pjpreeq  26185  cnvbraval  26898  cdj3lem2  27223  xdivmul  27491  cvmliftphtlem  28632  cvmlift3lem4  28637  cvmlift3lem6  28639  cvmlift3lem9  28642  transportprops  29656  ltflcei  30015  exidresid  30313  fourierdlem50  31828  usgedgvadf1lem2  32252  usgedgvadf1ALTlem2  32255  lshpkrlem1  34558  cdlemeiota  36034  dochfl1  36926  hgmapvs  37344
  Copyright terms: Public domain W3C validator