Theorem riota2 7402

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-nf 1816  df-sb 2099  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-ss 3896  df-un 4151  df-sn 4584  df-pr 4586  df-uni 4867  df-iota 6494  df-riota 7377

This theorem is used by:  eqsup  9448  sup0  9459  ttrcltr  9717  fin23lem22  10405  subadd  11560  divmul  11977  fllelt  13937  flflp1  13947  flval2  13954  flbi  13956  remim  15284  resqrtcl  15420  resqrtthlem  15421  sqrtneg  15434  sqrtthlem  15530  divalgmod  16576  qnumdenbi  16920  catidd  17854  lubprop  18530  glbprop  18543  poslubd  18585  isglbd  18683  ismgmid  18845  isgrpinv  19204  pj1id  19913  evlsval3  22398  coeeq  26546  cutbday  28170  eqcuts  28171  cutsun12  28176  cutbdaylt  28184  divmulsw  28579  ismir  29131  mireq  29137  ismidb  29283  islmib  29292  angmgmaddov1  29388  angmgmaddov2  29389  usgredg2vlem2  29807  frgrncvvdeqlem3  30902  frgr2wwlkeqm  30932  cnidOLD  31184  hilid  31763  pjpreeq  32000  cnvbraval  32712  cdj3lem2  33037  xdivmul  33491  cvmliftphtlem  36082  cvmlift3lem4  36087  cvmlift3lem6  36089  cvmlift3lem9  36092  transportprops  36799  ltflcei  38532  cmpidelt  38794  exidresid  38814  lshpkrlem1  40168  cdlemeiota  41643  dochfl1  42534  hgmapvs  42949  renegadd  43424  resubadd  43431  addinvcom  43484  redivmuld  43497  fsuppind  43619  wessf1ornlem  46200  fourierdlem50  47166