Theorem riota2 6533

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∃!wreu 2898  ℩crio 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-reu 2903  df-v 3175  df-sbc 3403  df-un 3545  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-riota 6511

This theorem is referenced by:  eqsup  8245  sup0  8255  fin23lem22  9032  subadd  10163  divmul  10567  fllelt  12460  flflp1  12470  flval2  12477  flbi  12479  remim  13705  resqrtcl  13842  resqrtthlem  13843  sqrtneg  13856  sqrtthlem  13950  divalgmod  14967  divalgmodOLD  14968  qnumdenbi  15290  catidd  16164  lubprop  16809  glbprop  16822  isglbd  16940  poslubd  16971  ismgmid  17087  isgrpinv  17295  pj1id  17935  coeeq  23787  ismir  25354  mireq  25360  ismidb  25470  islmib  25479  usgraidx2vlem2  25921  nbgraf1olem3  25972  frgrancvvdeqlem4  26560  cnidOLD  26821  hilid  27402  pjpreeq  27641  cnvbraval  28353  cdj3lem2  28678  xdivmul  28964  cvmliftphtlem  30553  cvmlift3lem4  30558  cvmlift3lem6  30560  cvmlift3lem9  30563  transportprops  31311  ltflcei  32567  cmpidelt  32828  exidresid  32848  lshpkrlem1  33415  cdlemeiota  34891  dochfl1  35783  hgmapvs  36201  wessf1ornlem  38366  fourierdlem50  39049  usgredg2vlem2  40453  frgrncvvdeqlem4  41472