Theorem riota2 7258

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∃!wreu 3066  ℩crio 7231

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-reu 3072  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564  df-uni 4840  df-iota 6391  df-riota 7232

This theorem is referenced by:  eqsup  9215  sup0  9225  ttrcltr  9474  fin23lem22  10083  subadd  11224  divmul  11636  fllelt  13517  flflp1  13527  flval2  13534  flbi  13536  remim  14828  resqrtcl  14965  resqrtthlem  14966  sqrtneg  14979  sqrtthlem  15074  divalgmod  16115  qnumdenbi  16448  catidd  17389  lubprop  18076  glbprop  18089  poslubd  18131  isglbd  18227  ismgmid  18349  isgrpinv  18632  pj1id  19305  coeeq  25388  ismir  27020  mireq  27026  ismidb  27139  islmib  27148  usgredg2vlem2  27593  frgrncvvdeqlem3  28665  frgr2wwlkeqm  28695  cnidOLD  28944  hilid  29523  pjpreeq  29760  cnvbraval  30472  cdj3lem2  30797  xdivmul  31199  cvmliftphtlem  33279  cvmlift3lem4  33284  cvmlift3lem6  33286  cvmlift3lem9  33289  scutbday  33998  eqscut  33999  scutun12  34004  scutbdaylt  34012  transportprops  34336  ltflcei  35765  cmpidelt  36017  exidresid  36037  lshpkrlem1  37124  cdlemeiota  38599  dochfl1  39490  hgmapvs  39905  evlsval3  40272  fsuppind  40279  renegadd  40355  resubadd  40362  addinvcom  40413  wessf1ornlem  42722  fourierdlem50  43697