Theorem riota2 7352

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

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

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 2185  ax-ext 2709

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ral 3053  df-rex 3063  df-reu 3353  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6458  df-riota 7327

This theorem is referenced by:  eqsup  9373  sup0  9384  ttrcltr  9639  fin23lem22  10251  subadd  11397  divmul  11813  fllelt  13731  flflp1  13741  flval2  13748  flbi  13750  remim  15054  resqrtcl  15190  resqrtthlem  15191  sqrtneg  15204  sqrtthlem  15300  divalgmod  16347  qnumdenbi  16685  catidd  17617  lubprop  18293  glbprop  18306  poslubd  18348  isglbd  18446  ismgmid  18604  isgrpinv  18940  pj1id  19645  evlsval3  22061  coeeq  26205  cutbday  27797  eqcuts  27798  cutsun12  27803  cutbdaylt  27811  divmulsw  28206  ismir  28749  mireq  28755  ismidb  28868  islmib  28877  usgredg2vlem2  29317  frgrncvvdeqlem3  30394  frgr2wwlkeqm  30424  cnidOLD  30676  hilid  31255  pjpreeq  31492  cnvbraval  32204  cdj3lem2  32529  xdivmul  33023  cvmliftphtlem  35539  cvmlift3lem4  35544  cvmlift3lem6  35546  cvmlift3lem9  35549  transportprops  36256  ltflcei  37888  cmpidelt  38139  exidresid  38159  lshpkrlem1  39515  cdlemeiota  40990  dochfl1  41881  hgmapvs  42296  renegadd  42771  resubadd  42778  addinvcom  42831  redivmuld  42844  fsuppind  42977  wessf1ornlem  45573  fourierdlem50  46543