Theorem riota2 7393

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∃!wreu 3373  ℩crio 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ral 3086  df-rex 3096  df-reu 3376  df-v 3463  df-un 3916  df-ss 3928  df-sn 4593  df-pr 4595  df-uni 4875  df-iota 6493  df-riota 7368

This theorem is referenced by:  eqsup  9416  sup0  9427  ttrcltr  9685  fin23lem22  10311  subadd  11460  divmul  11875  fllelt  13830  flflp1  13840  flval2  13847  flbi  13849  remim  15168  resqrtcl  15304  resqrtthlem  15305  sqrtneg  15318  sqrtthlem  15414  divalgmod  16464  qnumdenbi  16803  catidd  17736  lubprop  18412  glbprop  18425  poslubd  18467  isglbd  18565  ismgmid  18723  isgrpinv  19060  pj1id  19769  evlsval3  22209  coeeq  26353  cutbday  27943  eqcuts  27944  cutsun12  27949  cutbdaylt  27957  divmulsw  28352  ismir  28898  mireq  28904  ismidb  29045  islmib  29054  usgredg2vlem2  29517  frgrncvvdeqlem3  30593  frgr2wwlkeqm  30623  cnidOLD  30875  hilid  31454  pjpreeq  31691  cnvbraval  32403  cdj3lem2  32728  xdivmul  33185  cvmliftphtlem  35742  cvmlift3lem4  35747  cvmlift3lem6  35749  cvmlift3lem9  35752  transportprops  36459  ltflcei  38182  cmpidelt  38433  exidresid  38453  lshpkrlem1  39809  cdlemeiota  41284  dochfl1  42175  hgmapvs  42590  renegadd  43058  resubadd  43065  addinvcom  43118  redivmuld  43131  fsuppind  43249  wessf1ornlem  45830  fourierdlem50  46797