Theorem riota2 7391

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∃!wreu 3363  ℩crio 7365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-reu 3366  df-v 3452  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6484  df-riota 7366

This theorem is used by:  eqsup  9426  sup0  9437  ttrcltr  9695  fin23lem22  10362  subadd  11517  divmul  11932  fllelt  13891  flflp1  13901  flval2  13908  flbi  13910  remim  15237  resqrtcl  15373  resqrtthlem  15374  sqrtneg  15387  sqrtthlem  15483  divalgmod  16529  qnumdenbi  16868  catidd  17801  lubprop  18477  glbprop  18490  poslubd  18532  isglbd  18630  ismgmid  18792  isgrpinv  19151  pj1id  19860  evlsval3  22345  coeeq  26493  cutbday  28089  eqcuts  28090  cutsun12  28095  cutbdaylt  28103  divmulsw  28498  ismir  29050  mireq  29056  ismidb  29202  islmib  29211  angmgmaddov1  29307  angmgmaddov2  29308  usgredg2vlem2  29726  frgrncvvdeqlem3  30821  frgr2wwlkeqm  30851  cnidOLD  31103  hilid  31682  pjpreeq  31919  cnvbraval  32631  cdj3lem2  32956  xdivmul  33410  cvmliftphtlem  35997  cvmlift3lem4  36002  cvmlift3lem6  36004  cvmlift3lem9  36007  transportprops  36715  ltflcei  38445  cmpidelt  38707  exidresid  38727  lshpkrlem1  40081  cdlemeiota  41556  dochfl1  42447  hgmapvs  42862  renegadd  43345  resubadd  43352  addinvcom  43405  redivmuld  43418  fsuppind  43534  wessf1ornlem  46115  fourierdlem50  47082