Theorem riota2 6633

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

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 |- F/_ x B
2		nfv 1843	. 2 |- F/ x ps
3		riota2.1	. 2 |- ( x = B -> ( ph <-> ps ) )
4	1, 2, 3	riota2f 6632	1 |- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   E!wreu 2914   iota_crio 6610

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-reu 2919  df-v 3202  df-sbc 3436  df-un 3579  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-riota 6611

This theorem is referenced by:  eqsup  8362  sup0  8372  fin23lem22  9149  subadd  10284  divmul  10688  fllelt  12598  flflp1  12608  flval2  12615  flbi  12617  remim  13857  resqrtcl  13994  resqrtthlem  13995  sqrtneg  14008  sqrtthlem  14102  divalgmod  15129  divalgmodOLD  15130  qnumdenbi  15452  catidd  16341  lubprop  16986  glbprop  16999  isglbd  17117  poslubd  17148  ismgmid  17264  isgrpinv  17472  pj1id  18112  coeeq  23983  ismir  25554  mireq  25560  ismidb  25670  islmib  25679  usgredg2vlem2  26118  frgrncvvdeqlem3  27165  frgr2wwlkeqm  27195  cnidOLD  27437  hilid  28018  pjpreeq  28257  cnvbraval  28969  cdj3lem2  29294  xdivmul  29633  cvmliftphtlem  31299  cvmlift3lem4  31304  cvmlift3lem6  31306  cvmlift3lem9  31309  scutbday  31913  scutun12  31917  scutbdaylt  31922  transportprops  32141  ltflcei  33397  cmpidelt  33658  exidresid  33678  lshpkrlem1  34397  cdlemeiota  35873  dochfl1  36765  hgmapvs  37183  wessf1ornlem  39371  fourierdlem50  40373