Theorem riota2 7380

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ∃!wreu 3367  ℩crio 7354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ral 3079  df-rex 3089  df-reu 3370  df-v 3458  df-un 3911  df-ss 3923  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6479  df-riota 7355

This theorem is referenced by:  eqsup  9404  sup0  9415  ttrcltr  9673  fin23lem22  10286  subadd  11435  divmul  11850  fllelt  13809  flflp1  13819  flval2  13826  flbi  13828  remim  15146  resqrtcl  15282  resqrtthlem  15283  sqrtneg  15296  sqrtthlem  15392  divalgmod  16442  qnumdenbi  16781  catidd  17714  lubprop  18390  glbprop  18403  poslubd  18445  isglbd  18543  ismgmid  18701  isgrpinv  19037  pj1id  19741  evlsval3  22144  coeeq  26289  cutbday  27879  eqcuts  27880  cutsun12  27885  cutbdaylt  27893  divmulsw  28288  ismir  28834  mireq  28840  ismidb  28953  islmib  28962  usgredg2vlem2  29429  frgrncvvdeqlem3  30505  frgr2wwlkeqm  30535  cnidOLD  30787  hilid  31366  pjpreeq  31603  cnvbraval  32315  cdj3lem2  32640  xdivmul  33104  cvmliftphtlem  35672  cvmlift3lem4  35677  cvmlift3lem6  35679  cvmlift3lem9  35682  transportprops  36389  ltflcei  38112  cmpidelt  38363  exidresid  38383  lshpkrlem1  39739  cdlemeiota  41214  dochfl1  42105  hgmapvs  42520  renegadd  42986  resubadd  42993  addinvcom  43046  redivmuld  43059  fsuppind  43177  wessf1ornlem  45768  fourierdlem50  46735