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

Theorem cbvabv 2746
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvabv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvabv {𝑥𝜑} = {𝑦𝜓}
Distinct variable groups:   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvabv
StepHypRef Expression
1 nfv 1842 . 2 𝑦𝜑
2 nfv 1842 . 2 𝑥𝜓
3 cbvabv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvab 2745 1 {𝑥𝜑} = {𝑦𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1482  {cab 2607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-clab 2608  df-cleq 2614
This theorem is referenced by:  cdeqab1  3425  difjust  3574  unjust  3576  injust  3578  uniiunlem  3689  dfif3  4098  pwjust  4157  snjust  4174  intab  4505  intabs  4823  iotajust  5848  wfrlem1  7411  sbth  8077  cardprc  8803  iunfictbso  8934  aceq3lem  8940  isf33lem  9185  axdc3  9273  axdclem  9338  axdc  9340  genpv  9818  ltexpri  9862  recexpr  9870  supsr  9930  hashf1lem2  13235  cvbtrcl  13725  mertens  14612  4sq  15662  isuhgr  25949  isushgr  25950  isupgr  25973  isumgr  25984  isuspgr  26041  isusgr  26042  isconngr  27042  isconngr1  27043  isfrgr  27115  dispcmp  29911  eulerpart  30429  ballotlemfmpn  30541  bnj66  30915  bnj1234  31066  subfacp1lem6  31152  subfacp1  31153  dfon2lem3  31674  dfon2lem7  31678  frrlem1  31764  nosupdm  31834  f1omptsn  33164  ismblfin  33430  glbconxN  34490  eldioph3  37155  diophrex  37165  cbvcllem  37741  ssfiunibd  39342
  Copyright terms: Public domain W3C validator