Theorem riota2 7340

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

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

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 2183  ax-ext 2707

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 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ral 3051  df-rex 3060  df-reu 3350  df-v 3441  df-un 3905  df-ss 3917  df-sn 4580  df-pr 4582  df-uni 4863  df-iota 6447  df-riota 7315

This theorem is referenced by:  eqsup  9361  sup0  9372  ttrcltr  9627  fin23lem22  10239  subadd  11385  divmul  11801  fllelt  13719  flflp1  13729  flval2  13736  flbi  13738  remim  15042  resqrtcl  15178  resqrtthlem  15179  sqrtneg  15192  sqrtthlem  15288  divalgmod  16335  qnumdenbi  16673  catidd  17605  lubprop  18281  glbprop  18294  poslubd  18336  isglbd  18434  ismgmid  18592  isgrpinv  18925  pj1id  19630  evlsval3  22046  coeeq  26190  scutbday  27780  eqscut  27781  scutun12  27786  scutbdaylt  27794  divsmulw  28173  ismir  28712  mireq  28718  ismidb  28831  islmib  28840  usgredg2vlem2  29280  frgrncvvdeqlem3  30357  frgr2wwlkeqm  30387  cnidOLD  30638  hilid  31217  pjpreeq  31454  cnvbraval  32166  cdj3lem2  32491  xdivmul  32985  cvmliftphtlem  35490  cvmlift3lem4  35495  cvmlift3lem6  35497  cvmlift3lem9  35500  transportprops  36207  ltflcei  37778  cmpidelt  38029  exidresid  38049  lshpkrlem1  39405  cdlemeiota  40880  dochfl1  41771  hgmapvs  42186  renegadd  42664  resubadd  42671  addinvcom  42724  redivmuld  42737  fsuppind  42870  wessf1ornlem  45466  fourierdlem50  46437