Theorem riota2 7238

Description: This theorem shows a condition that allows us 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 2906	. 2 ⊢ Ⅎ𝑥𝐵
2		nfv 1918	. 2 ⊢ Ⅎ𝑥𝜓
3		riota2.1	. 2 ⊢ (𝑥 = 𝐵 → (𝜑 ↔ 𝜓))
4	1, 2, 3	riota2f 7237	1 ⊢ ((𝐵 ∈ 𝐴 ∧ ∃!𝑥 ∈ 𝐴 𝜑) → (𝜓 ↔ (℩𝑥 ∈ 𝐴 𝜑) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∃!wreu 3065  ℩crio 7211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-reu 3070  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-sn 4559  df-pr 4561  df-uni 4837  df-iota 6376  df-riota 7212

This theorem is referenced by:  eqsup  9145  sup0  9155  fin23lem22  10014  subadd  11154  divmul  11566  fllelt  13445  flflp1  13455  flval2  13462  flbi  13464  remim  14756  resqrtcl  14893  resqrtthlem  14894  sqrtneg  14907  sqrtthlem  15002  divalgmod  16043  qnumdenbi  16376  catidd  17306  lubprop  17991  glbprop  18004  poslubd  18046  isglbd  18142  ismgmid  18264  isgrpinv  18547  pj1id  19220  coeeq  25293  ismir  26924  mireq  26930  ismidb  27043  islmib  27052  usgredg2vlem2  27496  frgrncvvdeqlem3  28566  frgr2wwlkeqm  28596  cnidOLD  28845  hilid  29424  pjpreeq  29661  cnvbraval  30373  cdj3lem2  30698  xdivmul  31101  cvmliftphtlem  33179  cvmlift3lem4  33184  cvmlift3lem6  33186  cvmlift3lem9  33189  ttrcltr  33702  scutbday  33925  eqscut  33926  scutun12  33931  scutbdaylt  33939  transportprops  34263  ltflcei  35692  cmpidelt  35944  exidresid  35964  lshpkrlem1  37051  cdlemeiota  38526  dochfl1  39417  hgmapvs  39832  evlsval3  40195  fsuppind  40202  renegadd  40276  resubadd  40283  addinvcom  40334  wessf1ornlem  42611  fourierdlem50  43587