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

Theorem riota2 6587
 Description: This theorem shows a condition that allows us 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 2761 . 2 𝑥𝐵
2 nfv 1840 . 2 𝑥𝜓
3 riota2.1 . 2 (𝑥 = 𝐵 → (𝜑𝜓))
41, 2, 3riota2f 6586 1 ((𝐵𝐴 ∧ ∃!𝑥𝐴 𝜑) → (𝜓 ↔ (𝑥𝐴 𝜑) = 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∃!wreu 2909  ℩crio 6564 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-reu 2914  df-v 3188  df-sbc 3418  df-un 3560  df-sn 4149  df-pr 4151  df-uni 4403  df-iota 5810  df-riota 6565 This theorem is referenced by:  eqsup  8306  sup0  8316  fin23lem22  9093  subadd  10228  divmul  10632  fllelt  12538  flflp1  12548  flval2  12555  flbi  12557  remim  13791  resqrtcl  13928  resqrtthlem  13929  sqrtneg  13942  sqrtthlem  14036  divalgmod  15053  divalgmodOLD  15054  qnumdenbi  15376  catidd  16262  lubprop  16907  glbprop  16920  isglbd  17038  poslubd  17069  ismgmid  17185  isgrpinv  17393  pj1id  18033  coeeq  23887  ismir  25454  mireq  25460  ismidb  25570  islmib  25579  usgredg2vlem2  26011  frgrncvvdeqlem4  27030  cnidOLD  27283  hilid  27864  pjpreeq  28103  cnvbraval  28815  cdj3lem2  29140  xdivmul  29415  cvmliftphtlem  31004  cvmlift3lem4  31009  cvmlift3lem6  31011  cvmlift3lem9  31014  transportprops  31780  ltflcei  33026  cmpidelt  33287  exidresid  33307  lshpkrlem1  33874  cdlemeiota  35350  dochfl1  36242  hgmapvs  36660  wessf1ornlem  38842  fourierdlem50  39677
 Copyright terms: Public domain W3C validator