Theorem riota2 7342

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121  ∃!wreu 3344  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ral 3056  df-rex 3066  df-reu 3347  df-v 3435  df-un 3890  df-ss 3902  df-sn 4559  df-pr 4561  df-uni 4842  df-iota 6445  df-riota 7317

This theorem is referenced by:  eqsup  9363  sup0  9374  ttrcltr  9632  fin23lem22  10244  subadd  11391  divmul  11807  fllelt  13751  flflp1  13761  flval2  13768  flbi  13770  remim  15074  resqrtcl  15210  resqrtthlem  15211  sqrtneg  15224  sqrtthlem  15320  divalgmod  16370  qnumdenbi  16709  catidd  17641  lubprop  18317  glbprop  18330  poslubd  18372  isglbd  18470  ismgmid  18628  isgrpinv  18964  pj1id  19669  evlsval3  22069  coeeq  26214  cutbday  27798  eqcuts  27799  cutsun12  27804  cutbdaylt  27812  divmulsw  28207  ismir  28749  mireq  28755  ismidb  28868  islmib  28877  usgredg2vlem2  29317  frgrncvvdeqlem3  30393  frgr2wwlkeqm  30423  cnidOLD  30675  hilid  31254  pjpreeq  31491  cnvbraval  32203  cdj3lem2  32528  xdivmul  33007  cvmliftphtlem  35560  cvmlift3lem4  35565  cvmlift3lem6  35567  cvmlift3lem9  35570  transportprops  36277  ltflcei  37990  cmpidelt  38241  exidresid  38261  lshpkrlem1  39617  cdlemeiota  41092  dochfl1  41983  hgmapvs  42398  renegadd  42864  resubadd  42871  addinvcom  42924  redivmuld  42937  fsuppind  43055  wessf1ornlem  45646  fourierdlem50  46613