Theorem riota2 7322

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

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

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 3344  df-v 3435  df-un 3904  df-ss 3916  df-sn 4574  df-pr 4576  df-uni 4857  df-iota 6432  df-riota 7297

This theorem is referenced by:  eqsup  9334  sup0  9345  ttrcltr  9600  fin23lem22  10209  subadd  11354  divmul  11770  fllelt  13689  flflp1  13699  flval2  13706  flbi  13708  remim  15011  resqrtcl  15147  resqrtthlem  15148  sqrtneg  15161  sqrtthlem  15257  divalgmod  16304  qnumdenbi  16642  catidd  17573  lubprop  18249  glbprop  18262  poslubd  18304  isglbd  18402  ismgmid  18526  isgrpinv  18859  pj1id  19565  coeeq  26113  scutbday  27699  eqscut  27700  scutun12  27705  scutbdaylt  27713  divsmulw  28086  ismir  28591  mireq  28597  ismidb  28710  islmib  28719  usgredg2vlem2  29158  frgrncvvdeqlem3  30232  frgr2wwlkeqm  30262  cnidOLD  30513  hilid  31092  pjpreeq  31329  cnvbraval  32041  cdj3lem2  32366  xdivmul  32860  cvmliftphtlem  35307  cvmlift3lem4  35312  cvmlift3lem6  35314  cvmlift3lem9  35317  transportprops  36025  ltflcei  37605  cmpidelt  37856  exidresid  37876  lshpkrlem1  39106  cdlemeiota  40581  dochfl1  41472  hgmapvs  41887  renegadd  42362  resubadd  42369  addinvcom  42422  redivmuld  42435  evlsval3  42549  fsuppind  42580  wessf1ornlem  45179  fourierdlem50  46151