Theorem riota2 7331

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∃!wreu 3341  ℩crio 7305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-reu 3344  df-v 3438  df-un 3908  df-ss 3920  df-sn 4578  df-pr 4580  df-uni 4859  df-iota 6438  df-riota 7306

This theorem is referenced by:  eqsup  9346  sup0  9357  ttrcltr  9612  fin23lem22  10221  subadd  11366  divmul  11782  fllelt  13701  flflp1  13711  flval2  13718  flbi  13720  remim  15024  resqrtcl  15160  resqrtthlem  15161  sqrtneg  15174  sqrtthlem  15270  divalgmod  16317  qnumdenbi  16655  catidd  17586  lubprop  18262  glbprop  18275  poslubd  18317  isglbd  18415  ismgmid  18539  isgrpinv  18872  pj1id  19578  coeeq  26130  scutbday  27716  eqscut  27717  scutun12  27722  scutbdaylt  27730  divsmulw  28103  ismir  28608  mireq  28614  ismidb  28727  islmib  28736  usgredg2vlem2  29175  frgrncvvdeqlem3  30249  frgr2wwlkeqm  30279  cnidOLD  30530  hilid  31109  pjpreeq  31346  cnvbraval  32058  cdj3lem2  32383  xdivmul  32874  cvmliftphtlem  35310  cvmlift3lem4  35315  cvmlift3lem6  35317  cvmlift3lem9  35320  transportprops  36028  ltflcei  37608  cmpidelt  37859  exidresid  37879  lshpkrlem1  39109  cdlemeiota  40584  dochfl1  41475  hgmapvs  41890  renegadd  42365  resubadd  42372  addinvcom  42425  redivmuld  42438  evlsval3  42552  fsuppind  42583  wessf1ornlem  45183  fourierdlem50  46157