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  9645  fin23lem22  10256  subadd  11400  divmul  11816  fllelt  13735  flflp1  13745  flval2  13752  flbi  13754  remim  15059  resqrtcl  15195  resqrtthlem  15196  sqrtneg  15209  sqrtthlem  15305  divalgmod  16352  qnumdenbi  16690  catidd  17621  lubprop  18297  glbprop  18310  poslubd  18352  isglbd  18450  ismgmid  18574  isgrpinv  18907  pj1id  19613  coeeq  26165  scutbday  27750  eqscut  27751  scutun12  27756  scutbdaylt  27764  divsmulw  28136  ismir  28639  mireq  28645  ismidb  28758  islmib  28767  usgredg2vlem2  29206  frgrncvvdeqlem3  30280  frgr2wwlkeqm  30310  cnidOLD  30561  hilid  31140  pjpreeq  31377  cnvbraval  32089  cdj3lem2  32414  xdivmul  32895  cvmliftphtlem  35297  cvmlift3lem4  35302  cvmlift3lem6  35304  cvmlift3lem9  35307  transportprops  36015  ltflcei  37595  cmpidelt  37846  exidresid  37866  lshpkrlem1  39096  cdlemeiota  40572  dochfl1  41463  hgmapvs  41878  renegadd  42353  resubadd  42360  addinvcom  42413  redivmuld  42426  evlsval3  42540  fsuppind  42571  wessf1ornlem  45172  fourierdlem50  46147