Theorem riota2 7328

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∃!wreu 3344  ℩crio 7302

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ral 3048  df-rex 3057  df-reu 3347  df-v 3438  df-un 3902  df-ss 3914  df-sn 4574  df-pr 4576  df-uni 4857  df-iota 6437  df-riota 7303

This theorem is referenced by:  eqsup  9340  sup0  9351  ttrcltr  9606  fin23lem22  10218  subadd  11363  divmul  11779  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  18573  isgrpinv  18906  pj1id  19611  coeeq  26159  scutbday  27745  eqscut  27746  scutun12  27751  scutbdaylt  27759  divsmulw  28132  ismir  28637  mireq  28643  ismidb  28756  islmib  28765  usgredg2vlem2  29204  frgrncvvdeqlem3  30281  frgr2wwlkeqm  30311  cnidOLD  30562  hilid  31141  pjpreeq  31378  cnvbraval  32090  cdj3lem2  32415  xdivmul  32905  cvmliftphtlem  35361  cvmlift3lem4  35366  cvmlift3lem6  35368  cvmlift3lem9  35371  transportprops  36078  ltflcei  37647  cmpidelt  37898  exidresid  37918  lshpkrlem1  39208  cdlemeiota  40683  dochfl1  41574  hgmapvs  41989  renegadd  42464  resubadd  42471  addinvcom  42524  redivmuld  42537  evlsval3  42651  fsuppind  42682  wessf1ornlem  45281  fourierdlem50  46253