Theorem riota2 7391

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∃!wreu 3375  ℩crio 7364

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3063  df-rex 3072  df-reu 3378  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-riota 7365

This theorem is referenced by:  eqsup  9451  sup0  9461  ttrcltr  9711  fin23lem22  10322  subadd  11463  divmul  11875  fllelt  13762  flflp1  13772  flval2  13779  flbi  13781  remim  15064  resqrtcl  15200  resqrtthlem  15201  sqrtneg  15214  sqrtthlem  15309  divalgmod  16349  qnumdenbi  16680  catidd  17624  lubprop  18311  glbprop  18324  poslubd  18366  isglbd  18462  ismgmid  18584  isgrpinv  18878  pj1id  19567  coeeq  25741  scutbday  27305  eqscut  27306  scutun12  27311  scutbdaylt  27319  divsmulw  27640  ismir  27910  mireq  27916  ismidb  28029  islmib  28038  usgredg2vlem2  28483  frgrncvvdeqlem3  29554  frgr2wwlkeqm  29584  cnidOLD  29835  hilid  30414  pjpreeq  30651  cnvbraval  31363  cdj3lem2  31688  xdivmul  32091  cvmliftphtlem  34308  cvmlift3lem4  34313  cvmlift3lem6  34315  cvmlift3lem9  34318  transportprops  35006  ltflcei  36476  cmpidelt  36727  exidresid  36747  lshpkrlem1  37980  cdlemeiota  39456  dochfl1  40347  hgmapvs  40762  evlsval3  41131  fsuppind  41162  renegadd  41245  resubadd  41252  addinvcom  41304  wessf1ornlem  43882  fourierdlem50  44872