Theorem riota2 7338

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∃!wreu 3338  ℩crio 7312

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2184  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3050  df-rex 3060  df-reu 3341  df-v 3429  df-un 3890  df-ss 3902  df-sn 4558  df-pr 4560  df-uni 4841  df-iota 6443  df-riota 7313

This theorem is referenced by:  eqsup  9358  sup0  9369  ttrcltr  9626  fin23lem22  10238  subadd  11385  divmul  11801  fllelt  13745  flflp1  13755  flval2  13762  flbi  13764  remim  15068  resqrtcl  15204  resqrtthlem  15205  sqrtneg  15218  sqrtthlem  15314  divalgmod  16364  qnumdenbi  16703  catidd  17635  lubprop  18311  glbprop  18324  poslubd  18366  isglbd  18464  ismgmid  18622  isgrpinv  18958  pj1id  19663  evlsval3  22056  coeeq  26180  cutbday  27764  eqcuts  27765  cutsun12  27770  cutbdaylt  27778  divmulsw  28173  ismir  28715  mireq  28721  ismidb  28834  islmib  28843  usgredg2vlem2  29283  frgrncvvdeqlem3  30359  frgr2wwlkeqm  30389  cnidOLD  30641  hilid  31220  pjpreeq  31457  cnvbraval  32169  cdj3lem2  32494  xdivmul  32972  cvmliftphtlem  35487  cvmlift3lem4  35492  cvmlift3lem6  35494  cvmlift3lem9  35497  transportprops  36204  ltflcei  37917  cmpidelt  38168  exidresid  38188  lshpkrlem1  39544  cdlemeiota  41019  dochfl1  41910  hgmapvs  42325  renegadd  42792  resubadd  42799  addinvcom  42852  redivmuld  42865  fsuppind  43011  wessf1ornlem  45603  fourierdlem50  46572