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

Theorem riota2 6574
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 1630 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6573 1  |-  ( ( B  e.  A  /\  E! x  e.  A  ph )  ->  ( ps  <->  (
iota_ x  e.  A ph )  =  B
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653    e. wcel 1726   E!wreu 2709   iota_crio 6544
This theorem is referenced by:  eqsup  7463  fin23lem22  8209  subadd  9310  divmul  9683  uzinfmi  10557  fllelt  11208  flval2  11223  flbi  11225  remim  11924  resqrcl  12061  resqrthlem  12062  sqrneg  12075  sqrthlem  12168  divalgmod  12928  qnumdenbi  13138  catidd  13907  lubprop  14439  glbprop  14444  isglbd  14546  poslubd  14576  spwpr4  14665  ismgmid  14712  isgrpinv  14857  pj1id  15333  coeeq  20148  usgraidx2vlem2  21413  nbgraf1olem3  21455  cmpidelt  21919  cnid  21941  addinv  21942  mulid  21946  hilid  22665  pjpreeq  22902  cnvbraval  23615  cdj3lem2  23940  xdivmul  24173  cvmliftphtlem  25006  cvmlift3lem4  25011  cvmlift3lem6  25013  cvmlift3lem9  25016  transportprops  25970  ltflcei  26241  lxflflp1  26243  exidresid  26556  frgrancvvdeqlem4  28484  lshpkrlem1  29970  cdlemeiota  31444  dochfl1  32336  hgmapvs  32754
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-reu 2714  df-v 2960  df-sbc 3164  df-un 3327  df-if 3742  df-sn 3822  df-pr 3823  df-uni 4018  df-iota 5420  df-riota 6551
  Copyright terms: Public domain W3C validator