MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  riota2 Structured version   Visualization version   GIF version

Theorem riota2 7413
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
StepHypRef Expression
1 nfcv 2905 . 2 𝑥𝐵
2 nfv 1914 . 2 𝑥𝜓
3 riota2.1 . 2 (𝑥 = 𝐵 → (𝜑𝜓))
41, 2, 3riota2f 7412 1 ((𝐵𝐴 ∧ ∃!𝑥𝐴 𝜑) → (𝜓 ↔ (𝑥𝐴 𝜑) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2108  ∃!wreu 3378  crio 7387
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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ral 3062  df-rex 3071  df-reu 3381  df-v 3482  df-un 3956  df-ss 3968  df-sn 4627  df-pr 4629  df-uni 4908  df-iota 6514  df-riota 7388
This theorem is referenced by:  eqsup  9496  sup0  9506  ttrcltr  9756  fin23lem22  10367  subadd  11511  divmul  11925  fllelt  13837  flflp1  13847  flval2  13854  flbi  13856  remim  15156  resqrtcl  15292  resqrtthlem  15293  sqrtneg  15306  sqrtthlem  15401  divalgmod  16443  qnumdenbi  16781  catidd  17723  lubprop  18403  glbprop  18416  poslubd  18458  isglbd  18554  ismgmid  18678  isgrpinv  19011  pj1id  19717  coeeq  26266  scutbday  27849  eqscut  27850  scutun12  27855  scutbdaylt  27863  divsmulw  28218  ismir  28667  mireq  28673  ismidb  28786  islmib  28795  usgredg2vlem2  29243  frgrncvvdeqlem3  30320  frgr2wwlkeqm  30350  cnidOLD  30601  hilid  31180  pjpreeq  31417  cnvbraval  32129  cdj3lem2  32454  xdivmul  32907  cvmliftphtlem  35322  cvmlift3lem4  35327  cvmlift3lem6  35329  cvmlift3lem9  35332  transportprops  36035  ltflcei  37615  cmpidelt  37866  exidresid  37886  lshpkrlem1  39111  cdlemeiota  40587  dochfl1  41478  hgmapvs  41893  renegadd  42402  resubadd  42409  addinvcom  42461  evlsval3  42569  fsuppind  42600  wessf1ornlem  45190  fourierdlem50  46171
  Copyright terms: Public domain W3C validator