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

Theorem riota2 7351
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 2891 . 2 𝑥𝐵
2 nfv 1914 . 2 𝑥𝜓
3 riota2.1 . 2 (𝑥 = 𝐵 → (𝜑𝜓))
41, 2, 3riota2f 7350 1 ((𝐵𝐴 ∧ ∃!𝑥𝐴 𝜑) → (𝜓 ↔ (𝑥𝐴 𝜑) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1540  wcel 2109  ∃!wreu 3349  crio 7325
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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ral 3045  df-rex 3054  df-reu 3352  df-v 3446  df-un 3916  df-ss 3928  df-sn 4586  df-pr 4588  df-uni 4868  df-iota 6452  df-riota 7326
This theorem is referenced by:  eqsup  9383  sup0  9394  ttrcltr  9647  fin23lem22  10258  subadd  11402  divmul  11818  fllelt  13737  flflp1  13747  flval2  13754  flbi  13756  remim  15060  resqrtcl  15196  resqrtthlem  15197  sqrtneg  15210  sqrtthlem  15306  divalgmod  16353  qnumdenbi  16691  catidd  17622  lubprop  18298  glbprop  18311  poslubd  18353  isglbd  18451  ismgmid  18575  isgrpinv  18908  pj1id  19614  coeeq  26166  scutbday  27751  eqscut  27752  scutun12  27757  scutbdaylt  27765  divsmulw  28137  ismir  28640  mireq  28646  ismidb  28759  islmib  28768  usgredg2vlem2  29207  frgrncvvdeqlem3  30281  frgr2wwlkeqm  30311  cnidOLD  30562  hilid  31141  pjpreeq  31378  cnvbraval  32090  cdj3lem2  32415  xdivmul  32896  cvmliftphtlem  35298  cvmlift3lem4  35303  cvmlift3lem6  35305  cvmlift3lem9  35308  transportprops  36016  ltflcei  37596  cmpidelt  37847  exidresid  37867  lshpkrlem1  39097  cdlemeiota  40573  dochfl1  41464  hgmapvs  41879  renegadd  42354  resubadd  42361  addinvcom  42414  redivmuld  42427  evlsval3  42541  fsuppind  42572  wessf1ornlem  45173  fourierdlem50  46148
  Copyright terms: Public domain W3C validator