Theorem riota2 7372

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃!wreu 3354  ℩crio 7346

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702

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 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-reu 3357  df-v 3452  df-un 3922  df-ss 3934  df-sn 4593  df-pr 4595  df-uni 4875  df-iota 6467  df-riota 7347

This theorem is referenced by:  eqsup  9414  sup0  9425  ttrcltr  9676  fin23lem22  10287  subadd  11431  divmul  11847  fllelt  13766  flflp1  13776  flval2  13783  flbi  13785  remim  15090  resqrtcl  15226  resqrtthlem  15227  sqrtneg  15240  sqrtthlem  15336  divalgmod  16383  qnumdenbi  16721  catidd  17648  lubprop  18324  glbprop  18337  poslubd  18379  isglbd  18475  ismgmid  18599  isgrpinv  18932  pj1id  19636  coeeq  26139  scutbday  27723  eqscut  27724  scutun12  27729  scutbdaylt  27737  divsmulw  28103  ismir  28593  mireq  28599  ismidb  28712  islmib  28721  usgredg2vlem2  29160  frgrncvvdeqlem3  30237  frgr2wwlkeqm  30267  cnidOLD  30518  hilid  31097  pjpreeq  31334  cnvbraval  32046  cdj3lem2  32371  xdivmul  32852  cvmliftphtlem  35311  cvmlift3lem4  35316  cvmlift3lem6  35318  cvmlift3lem9  35321  transportprops  36029  ltflcei  37609  cmpidelt  37860  exidresid  37880  lshpkrlem1  39110  cdlemeiota  40586  dochfl1  41477  hgmapvs  41892  renegadd  42367  resubadd  42374  addinvcom  42427  redivmuld  42440  evlsval3  42554  fsuppind  42585  wessf1ornlem  45186  fourierdlem50  46161