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

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
StepHypRef Expression
1 nfcv 2908 . 2 𝑥𝐵
2 nfv 1918 . 2 𝑥𝜓
3 riota2.1 . 2 (𝑥 = 𝐵 → (𝜑𝜓))
41, 2, 3riota2f 7339 1 ((𝐵𝐴 ∧ ∃!𝑥𝐴 𝜑) → (𝜓 ↔ (𝑥𝐴 𝜑) = 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  ∃!wreu 3352  crio 7313
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-reu 3355  df-v 3448  df-un 3916  df-in 3918  df-ss 3928  df-sn 4588  df-pr 4590  df-uni 4867  df-iota 6449  df-riota 7314
This theorem is referenced by:  eqsup  9393  sup0  9403  ttrcltr  9653  fin23lem22  10264  subadd  11405  divmul  11817  fllelt  13703  flflp1  13713  flval2  13720  flbi  13722  remim  15003  resqrtcl  15139  resqrtthlem  15140  sqrtneg  15153  sqrtthlem  15248  divalgmod  16289  qnumdenbi  16620  catidd  17561  lubprop  18248  glbprop  18261  poslubd  18303  isglbd  18399  ismgmid  18521  isgrpinv  18805  pj1id  19482  coeeq  25591  scutbday  27146  eqscut  27147  scutun12  27152  scutbdaylt  27160  ismir  27604  mireq  27610  ismidb  27723  islmib  27732  usgredg2vlem2  28177  frgrncvvdeqlem3  29248  frgr2wwlkeqm  29278  cnidOLD  29527  hilid  30106  pjpreeq  30343  cnvbraval  31055  cdj3lem2  31380  xdivmul  31784  cvmliftphtlem  33914  cvmlift3lem4  33919  cvmlift3lem6  33921  cvmlift3lem9  33924  transportprops  34622  ltflcei  36069  cmpidelt  36321  exidresid  36341  lshpkrlem1  37575  cdlemeiota  39051  dochfl1  39942  hgmapvs  40357  evlsval3  40747  fsuppind  40768  renegadd  40844  resubadd  40851  addinvcom  40903  wessf1ornlem  43410  fourierdlem50  44404
  Copyright terms: Public domain W3C validator