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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-reu 3381  df-v 3482  df-un 3956  df-ss 3968  df-sn 4627  df-pr 4629  df-uni 4908  df-iota 6514  df-riota 7388

This theorem is referenced by:  eqsup  9496  sup0  9506  ttrcltr  9756  fin23lem22  10367  subadd  11511  divmul  11925  fllelt  13837  flflp1  13847  flval2  13854  flbi  13856  remim  15156  resqrtcl  15292  resqrtthlem  15293  sqrtneg  15306  sqrtthlem  15401  divalgmod  16443  qnumdenbi  16781  catidd  17723  lubprop  18403  glbprop  18416  poslubd  18458  isglbd  18554  ismgmid  18678  isgrpinv  19011  pj1id  19717  coeeq  26266  scutbday  27849  eqscut  27850  scutun12  27855  scutbdaylt  27863  divsmulw  28218  ismir  28667  mireq  28673  ismidb  28786  islmib  28795  usgredg2vlem2  29243  frgrncvvdeqlem3  30320  frgr2wwlkeqm  30350  cnidOLD  30601  hilid  31180  pjpreeq  31417  cnvbraval  32129  cdj3lem2  32454  xdivmul  32907  cvmliftphtlem  35322  cvmlift3lem4  35327  cvmlift3lem6  35329  cvmlift3lem9  35332  transportprops  36035  ltflcei  37615  cmpidelt  37866  exidresid  37886  lshpkrlem1  39111  cdlemeiota  40587  dochfl1  41478  hgmapvs  41893  renegadd  42402  resubadd  42409  addinvcom  42461  evlsval3  42569  fsuppind  42600  wessf1ornlem  45190  fourierdlem50  46171