Theorem riota2 7138

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∃!wreu 3140  ℩crio 7112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  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 3772  df-un 3940  df-in 3942  df-ss 3951  df-sn 4567  df-pr 4569  df-uni 4838  df-iota 6313  df-riota 7113

This theorem is referenced by:  eqsup  8919  sup0  8929  fin23lem22  9748  subadd  10888  divmul  11300  fllelt  13166  flflp1  13176  flval2  13183  flbi  13185  remim  14475  resqrtcl  14612  resqrtthlem  14613  sqrtneg  14626  sqrtthlem  14721  divalgmod  15756  qnumdenbi  16083  catidd  16950  lubprop  17595  glbprop  17608  isglbd  17726  poslubd  17757  ismgmid  17874  isgrpinv  18155  pj1id  18824  coeeq  24816  ismir  26444  mireq  26450  ismidb  26563  islmib  26572  usgredg2vlem2  27007  frgrncvvdeqlem3  28079  frgr2wwlkeqm  28109  cnidOLD  28358  hilid  28937  pjpreeq  29174  cnvbraval  29886  cdj3lem2  30211  xdivmul  30601  cvmliftphtlem  32564  cvmlift3lem4  32569  cvmlift3lem6  32571  cvmlift3lem9  32574  scutbday  33267  scutun12  33271  scutbdaylt  33276  transportprops  33495  ltflcei  34879  cmpidelt  35136  exidresid  35156  lshpkrlem1  36245  cdlemeiota  37720  dochfl1  38611  hgmapvs  39026  renegadd  39200  resubadd  39207  wessf1ornlem  41443  fourierdlem50  42440