Theorem riota2 6857

Description: This theorem shows a condition that allows us 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 2948	. 2 ⊢ Ⅎ𝑥𝐵
2		nfv 2005	. 2 ⊢ Ⅎ𝑥𝜓
3		riota2.1	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
4	1, 2, 3	riota2f 6856	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 197   ∧ wa 384   = wceq 1637   ∈ wcel 2156  ∃!wreu 3098  ℩crio 6834

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-reu 3103  df-v 3393  df-sbc 3634  df-un 3774  df-sn 4371  df-pr 4373  df-uni 4631  df-iota 6064  df-riota 6835

This theorem is referenced by:  eqsup  8601  sup0  8611  fin23lem22  9434  subadd  10569  divmul  10973  fllelt  12822  flflp1  12832  flval2  12839  flbi  12841  remim  14080  resqrtcl  14217  resqrtthlem  14218  sqrtneg  14231  sqrtthlem  14325  divalgmod  15349  qnumdenbi  15669  catidd  16545  lubprop  17191  glbprop  17204  isglbd  17322  poslubd  17353  ismgmid  17469  isgrpinv  17677  pj1id  18313  coeeq  24197  ismir  25768  mireq  25774  ismidb  25884  islmib  25893  usgredg2vlem2  26333  frgrncvvdeqlem3  27476  frgr2wwlkeqm  27506  cnidOLD  27765  hilid  28346  pjpreeq  28585  cnvbraval  29297  cdj3lem2  29622  xdivmul  29958  cvmliftphtlem  31622  cvmlift3lem4  31627  cvmlift3lem6  31629  cvmlift3lem9  31632  scutbday  32234  scutun12  32238  scutbdaylt  32243  transportprops  32462  ltflcei  33710  cmpidelt  33969  exidresid  33989  lshpkrlem1  34890  cdlemeiota  36366  dochfl1  37257  hgmapvs  37672  wessf1ornlem  39860  fourierdlem50  40852