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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!wreu 3349  ℩crio 7316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3062  df-reu 3352  df-v 3443  df-un 3907  df-ss 3919  df-sn 4582  df-pr 4584  df-uni 4865  df-iota 6449  df-riota 7317

This theorem is referenced by:  eqsup  9363  sup0  9374  ttrcltr  9629  fin23lem22  10241  subadd  11387  divmul  11803  fllelt  13721  flflp1  13731  flval2  13738  flbi  13740  remim  15044  resqrtcl  15180  resqrtthlem  15181  sqrtneg  15194  sqrtthlem  15290  divalgmod  16337  qnumdenbi  16675  catidd  17607  lubprop  18283  glbprop  18296  poslubd  18338  isglbd  18436  ismgmid  18594  isgrpinv  18927  pj1id  19632  evlsval3  22048  coeeq  26192  cutbday  27784  eqcuts  27785  cutsun12  27790  cutbdaylt  27798  divmulsw  28193  ismir  28735  mireq  28741  ismidb  28854  islmib  28863  usgredg2vlem2  29303  frgrncvvdeqlem3  30380  frgr2wwlkeqm  30410  cnidOLD  30661  hilid  31240  pjpreeq  31477  cnvbraval  32189  cdj3lem2  32514  xdivmul  33008  cvmliftphtlem  35513  cvmlift3lem4  35518  cvmlift3lem6  35520  cvmlift3lem9  35523  transportprops  36230  ltflcei  37811  cmpidelt  38062  exidresid  38082  lshpkrlem1  39438  cdlemeiota  40913  dochfl1  41804  hgmapvs  42219  renegadd  42694  resubadd  42701  addinvcom  42754  redivmuld  42767  fsuppind  42900  wessf1ornlem  45496  fourierdlem50  46467