Theorem riota2 7430

Description: This theorem shows a condition that allows to represent a descriptor with a class expression 𝐵. (Contributed by NM, 23-Aug-2011.) (Revised by Mario Carneiro, 10-Dec-2016.)

Hypothesis

Ref	Expression
riota2.1	⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
riota2	⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Distinct variable groups:   𝜓,𝑥   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem riota2

Step	Hyp	Ref	Expression
1		nfcv 2908	. 2 ⊢ Ⅎ𝑥𝐵
2		nfv 1913	. 2 ⊢ Ⅎ𝑥𝜓
3		riota2.1	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
4	1, 2, 3	riota2f 7429	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  ∃!wreu 3386  ℩crio 7403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ral 3068  df-rex 3077  df-reu 3389  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525  df-riota 7404

This theorem is referenced by:  eqsup  9525  sup0  9535  ttrcltr  9785  fin23lem22  10396  subadd  11539  divmul  11952  fllelt  13848  flflp1  13858  flval2  13865  flbi  13867  remim  15166  resqrtcl  15302  resqrtthlem  15303  sqrtneg  15316  sqrtthlem  15411  divalgmod  16454  qnumdenbi  16791  catidd  17738  lubprop  18428  glbprop  18441  poslubd  18483  isglbd  18579  ismgmid  18703  isgrpinv  19033  pj1id  19741  coeeq  26286  scutbday  27867  eqscut  27868  scutun12  27873  scutbdaylt  27881  divsmulw  28236  ismir  28685  mireq  28691  ismidb  28804  islmib  28813  usgredg2vlem2  29261  frgrncvvdeqlem3  30333  frgr2wwlkeqm  30363  cnidOLD  30614  hilid  31193  pjpreeq  31430  cnvbraval  32142  cdj3lem2  32467  xdivmul  32889  cvmliftphtlem  35285  cvmlift3lem4  35290  cvmlift3lem6  35292  cvmlift3lem9  35295  transportprops  35998  ltflcei  37568  cmpidelt  37819  exidresid  37839  lshpkrlem1  39066  cdlemeiota  40542  dochfl1  41433  hgmapvs  41848  renegadd  42348  resubadd  42355  addinvcom  42407  evlsval3  42514  fsuppind  42545  wessf1ornlem  45092  fourierdlem50  46077