Theorem riota2 7139

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∃!wreu 3140  ℩crio 7113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-reu 3145  df-v 3496  df-sbc 3773  df-un 3941  df-in 3943  df-ss 3952  df-sn 4568  df-pr 4570  df-uni 4839  df-iota 6314  df-riota 7114

This theorem is referenced by:  eqsup  8920  sup0  8930  fin23lem22  9749  subadd  10889  divmul  11301  fllelt  13168  flflp1  13178  flval2  13185  flbi  13187  remim  14476  resqrtcl  14613  resqrtthlem  14614  sqrtneg  14627  sqrtthlem  14722  divalgmod  15757  qnumdenbi  16084  catidd  16951  lubprop  17596  glbprop  17609  isglbd  17727  poslubd  17758  ismgmid  17875  isgrpinv  18156  pj1id  18825  coeeq  24817  ismir  26445  mireq  26451  ismidb  26564  islmib  26573  usgredg2vlem2  27008  frgrncvvdeqlem3  28080  frgr2wwlkeqm  28110  cnidOLD  28359  hilid  28938  pjpreeq  29175  cnvbraval  29887  cdj3lem2  30212  xdivmul  30601  cvmliftphtlem  32564  cvmlift3lem4  32569  cvmlift3lem6  32571  cvmlift3lem9  32574  scutbday  33267  scutun12  33271  scutbdaylt  33276  transportprops  33495  ltflcei  34895  cmpidelt  35152  exidresid  35172  lshpkrlem1  36261  cdlemeiota  37736  dochfl1  38627  hgmapvs  39042  renegadd  39222  resubadd  39229  wessf1ornlem  41465  fourierdlem50  42461