Theorem riota2 7387

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 2898	. 2 ⊢ Ⅎ𝑥𝐵
2		nfv 1914	. 2 ⊢ Ⅎ𝑥𝜓
3		riota2.1	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
4	1, 2, 3	riota2f 7386	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∃!wreu 3357  ℩crio 7361

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ral 3052  df-rex 3061  df-reu 3360  df-v 3461  df-un 3931  df-ss 3943  df-sn 4602  df-pr 4604  df-uni 4884  df-iota 6484  df-riota 7362

This theorem is referenced by:  eqsup  9468  sup0  9479  ttrcltr  9730  fin23lem22  10341  subadd  11485  divmul  11899  fllelt  13814  flflp1  13824  flval2  13831  flbi  13833  remim  15136  resqrtcl  15272  resqrtthlem  15273  sqrtneg  15286  sqrtthlem  15381  divalgmod  16425  qnumdenbi  16763  catidd  17692  lubprop  18368  glbprop  18381  poslubd  18423  isglbd  18519  ismgmid  18643  isgrpinv  18976  pj1id  19680  coeeq  26184  scutbday  27768  eqscut  27769  scutun12  27774  scutbdaylt  27782  divsmulw  28148  ismir  28638  mireq  28644  ismidb  28757  islmib  28766  usgredg2vlem2  29205  frgrncvvdeqlem3  30282  frgr2wwlkeqm  30312  cnidOLD  30563  hilid  31142  pjpreeq  31379  cnvbraval  32091  cdj3lem2  32416  xdivmul  32899  cvmliftphtlem  35339  cvmlift3lem4  35344  cvmlift3lem6  35346  cvmlift3lem9  35349  transportprops  36052  ltflcei  37632  cmpidelt  37883  exidresid  37903  lshpkrlem1  39128  cdlemeiota  40604  dochfl1  41495  hgmapvs  41910  renegadd  42415  resubadd  42422  addinvcom  42474  evlsval3  42582  fsuppind  42613  wessf1ornlem  45209  fourierdlem50  46185