Theorem riota2 7413

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2106  ∃!wreu 3376  ℩crio 7387

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ral 3060  df-rex 3069  df-reu 3379  df-v 3480  df-un 3968  df-ss 3980  df-sn 4632  df-pr 4634  df-uni 4913  df-iota 6516  df-riota 7388

This theorem is referenced by:  eqsup  9494  sup0  9504  ttrcltr  9754  fin23lem22  10365  subadd  11509  divmul  11923  fllelt  13834  flflp1  13844  flval2  13851  flbi  13853  remim  15153  resqrtcl  15289  resqrtthlem  15290  sqrtneg  15303  sqrtthlem  15398  divalgmod  16440  qnumdenbi  16778  catidd  17725  lubprop  18416  glbprop  18429  poslubd  18471  isglbd  18567  ismgmid  18691  isgrpinv  19024  pj1id  19732  coeeq  26281  scutbday  27864  eqscut  27865  scutun12  27870  scutbdaylt  27878  divsmulw  28233  ismir  28682  mireq  28688  ismidb  28801  islmib  28810  usgredg2vlem2  29258  frgrncvvdeqlem3  30330  frgr2wwlkeqm  30360  cnidOLD  30611  hilid  31190  pjpreeq  31427  cnvbraval  32139  cdj3lem2  32464  xdivmul  32892  cvmliftphtlem  35302  cvmlift3lem4  35307  cvmlift3lem6  35309  cvmlift3lem9  35312  transportprops  36016  ltflcei  37595  cmpidelt  37846  exidresid  37866  lshpkrlem1  39092  cdlemeiota  40568  dochfl1  41459  hgmapvs  41874  renegadd  42379  resubadd  42386  addinvcom  42438  evlsval3  42546  fsuppind  42577  wessf1ornlem  45128  fourierdlem50  46112