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

Theorem riota2 6183
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 2616 . 2  |-  F/_ x B
2 nfv 1674 . 2  |-  F/ x ps
3 riota2.1 . 2  |-  ( x  =  B  ->  ( ph 
<->  ps ) )
41, 2, 3riota2f 6182 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 1370    e. wcel 1758   E!wreu 2800   iota_crio 6159
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2803  df-rex 2804  df-reu 2805  df-v 3078  df-sbc 3293  df-un 3440  df-sn 3985  df-pr 3987  df-uni 4199  df-iota 5488  df-riota 6160
This theorem is referenced by:  eqsup  7816  fin23lem22  8606  subadd  9723  divmul  10107  uzinfmi  11044  fllelt  11763  flval2  11778  flbi  11780  remim  12723  resqrcl  12860  resqrthlem  12861  sqrneg  12874  sqrthlem  12967  divalgmod  13727  qnumdenbi  13939  catidd  14736  lubprop  15274  glbprop  15287  isglbd  15405  poslubd  15436  ismgmid  15553  isgrpinv  15706  pj1id  16316  coeeq  21827  ismir  23205  mireq  23211  usgraidx2vlem2  23461  nbgraf1olem3  23503  cmpidelt  23967  cnid  23989  addinv  23990  mulid  23994  hilid  24714  pjpreeq  24952  cnvbraval  25665  cdj3lem2  25990  xdivmul  26244  cvmliftphtlem  27349  cvmlift3lem4  27354  cvmlift3lem6  27356  cvmlift3lem9  27359  transportprops  28208  ltflcei  28566  lxflflp1  28568  exidresid  28891  frgrancvvdeqlem4  30773  lshpkrlem1  33078  cdlemeiota  34552  dochfl1  35444  hgmapvs  35862
  Copyright terms: Public domain W3C validator