Theorem riota2 7398

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734

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 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ral 3079  df-rex 3089  df-reu 3368  df-v 3455  df-un 3907  df-ss 3919  df-sn 4588  df-pr 4590  df-uni 4871  df-iota 6493  df-riota 7373

This theorem is used by:  eqsup  9429  sup0  9440  ttrcltr  9698  fin23lem22  10332  subadd  11487  divmul  11902  fllelt  13860  flflp1  13870  flval2  13877  flbi  13879  remim  15206  resqrtcl  15342  resqrtthlem  15343  sqrtneg  15356  sqrtthlem  15452  divalgmod  16500  qnumdenbi  16839  catidd  17772  lubprop  18448  glbprop  18461  poslubd  18503  isglbd  18601  ismgmid  18762  isgrpinv  19118  pj1id  19827  evlsval3  22306  coeeq  26454  cutbday  28047  eqcuts  28048  cutsun12  28053  cutbdaylt  28061  divmulsw  28456  ismir  29008  mireq  29014  ismidb  29160  islmib  29169  angmndaddov1  29261  angmndaddov2  29262  usgredg2vlem2  29672  frgrncvvdeqlem3  30767  frgr2wwlkeqm  30797  cnidOLD  31049  hilid  31628  pjpreeq  31865  cnvbraval  32577  cdj3lem2  32902  xdivmul  33357  cvmliftphtlem  35883  cvmlift3lem4  35888  cvmlift3lem6  35890  cvmlift3lem9  35893  transportprops  36601  ltflcei  38349  cmpidelt  38596  exidresid  38616  lshpkrlem1  39970  cdlemeiota  41445  dochfl1  42336  hgmapvs  42751  renegadd  43234  resubadd  43241  addinvcom  43294  redivmuld  43307  fsuppind  43423  wessf1ornlem  46004  fourierdlem50  46971