Theorem riota2 7352

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 7351	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

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

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 6453  df-riota 7327

This theorem is referenced by:  eqsup  9384  sup0  9395  ttrcltr  9648  fin23lem22  10259  subadd  11403  divmul  11819  fllelt  13738  flflp1  13748  flval2  13755  flbi  13757  remim  15061  resqrtcl  15197  resqrtthlem  15198  sqrtneg  15211  sqrtthlem  15307  divalgmod  16354  qnumdenbi  16692  catidd  17623  lubprop  18299  glbprop  18312  poslubd  18354  isglbd  18452  ismgmid  18576  isgrpinv  18909  pj1id  19615  coeeq  26167  scutbday  27752  eqscut  27753  scutun12  27758  scutbdaylt  27766  divsmulw  28138  ismir  28641  mireq  28647  ismidb  28760  islmib  28769  usgredg2vlem2  29208  frgrncvvdeqlem3  30282  frgr2wwlkeqm  30312  cnidOLD  30563  hilid  31142  pjpreeq  31379  cnvbraval  32091  cdj3lem2  32416  xdivmul  32897  cvmliftphtlem  35299  cvmlift3lem4  35304  cvmlift3lem6  35306  cvmlift3lem9  35309  transportprops  36017  ltflcei  37597  cmpidelt  37848  exidresid  37868  lshpkrlem1  39098  cdlemeiota  40574  dochfl1  41465  hgmapvs  41880  renegadd  42355  resubadd  42362  addinvcom  42415  redivmuld  42428  evlsval3  42542  fsuppind  42573  wessf1ornlem  45174  fourierdlem50  46149