Theorem riota2 5622

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 2228	. 2 |- F/_ x B
2		nfv 1466	. 2 |- F/ x ps
3		riota2.1	. 2 |- ( x = B -> ( ph <-> ps ) )
4	1, 2, 3	riota2f 5621	1 |- ( ( B e. A /\ E! x e. A ph ) -> ( ps <-> ( iota_ x e. A ph ) = B ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1289   e. wcel 1438   E!wreu 2361   iota_crio 5599

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-rex 2365  df-reu 2366  df-v 2621  df-sbc 2841  df-un 3003  df-sn 3450  df-pr 3451  df-uni 3652  df-iota 4975  df-riota 5600

This theorem is referenced by:  eqsupti  6681  prsrriota  7323  recriota  7415  axcaucvglemval  7422  subadd  7675  divmulap  8132  flqlelt  9671  flqbi  9685  remim  10282  resqrtcl  10450  rersqrtthlem  10451  divalgmod  11192  dfgcd3  11264  bezout  11265  oddpwdclemxy  11412  qnumdenbi  11435