Theorem riota2 7422

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  ∃!wreu 3367  ℩crio 7396

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-reu 3370  df-v 3456  df-ss 3901  df-un 4154  df-sn 4589  df-pr 4591  df-uni 4871  df-iota 6509  df-riota 7397

This theorem is used by:  eqsup  9472  sup0  9483  ttrcltr  9741  fin23lem22  10429  subadd  11584  divmul  12001  fllelt  13961  flflp1  13971  flval2  13978  flbi  13980  remim  15310  resqrtcl  15446  resqrtthlem  15447  sqrtneg  15460  sqrtthlem  15556  divalgmod  16602  qnumdenbi  16946  catidd  17880  lubprop  18556  glbprop  18569  poslubd  18611  isglbd  18709  ismgmid  18871  isgrpinv  19230  pj1id  19940  evlsval3  22425  coeeq  26573  cutbday  28197  eqcuts  28198  cutsun12  28203  cutbdaylt  28211  divmulsw  28606  ismir  29158  mireq  29164  ismidb  29310  islmib  29319  angmgmaddov1  29415  angmgmaddov2  29416  usgredg2vlem2  29834  frgrncvvdeqlem3  30929  frgr2wwlkeqm  30959  cnidOLD  31211  hilid  31790  pjpreeq  32027  cnvbraval  32739  cdj3lem2  33064  xdivmul  33558  cvmliftphtlem  36248  cvmlift3lem4  36253  cvmlift3lem6  36255  cvmlift3lem9  36258  transportprops  36976  ltflcei  38722  cmpidelt  38984  exidresid  39004  lshpkrlem1  40358  cdlemeiota  41833  dochfl1  42724  hgmapvs  43139  renegadd  43614  resubadd  43621  addinvcom  43674  redivmuld  43687  fsuppind  43809  wessf1ornlem  46403  fourierdlem50  47369