Theorem riota2 7351

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

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

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 2701

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-reu 3352  df-v 3446  df-un 3916  df-ss 3928  df-sn 4586  df-pr 4588  df-uni 4868  df-iota 6452  df-riota 7326

This theorem is referenced by:  eqsup  9383  sup0  9394  ttrcltr  9647  fin23lem22  10258  subadd  11402  divmul  11818  fllelt  13737  flflp1  13747  flval2  13754  flbi  13756  remim  15060  resqrtcl  15196  resqrtthlem  15197  sqrtneg  15210  sqrtthlem  15306  divalgmod  16353  qnumdenbi  16691  catidd  17622  lubprop  18298  glbprop  18311  poslubd  18353  isglbd  18451  ismgmid  18575  isgrpinv  18908  pj1id  19614  coeeq  26166  scutbday  27751  eqscut  27752  scutun12  27757  scutbdaylt  27765  divsmulw  28137  ismir  28640  mireq  28646  ismidb  28759  islmib  28768  usgredg2vlem2  29207  frgrncvvdeqlem3  30281  frgr2wwlkeqm  30311  cnidOLD  30562  hilid  31141  pjpreeq  31378  cnvbraval  32090  cdj3lem2  32415  xdivmul  32896  cvmliftphtlem  35298  cvmlift3lem4  35303  cvmlift3lem6  35305  cvmlift3lem9  35308  transportprops  36016  ltflcei  37596  cmpidelt  37847  exidresid  37867  lshpkrlem1  39097  cdlemeiota  40573  dochfl1  41464  hgmapvs  41879  renegadd  42354  resubadd  42361  addinvcom  42414  redivmuld  42427  evlsval3  42541  fsuppind  42572  wessf1ornlem  45173  fourierdlem50  46148