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

Theorem cbvabv 2729
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 1828 . 2 𝑦𝜑
2 nfv 1828 . 2 𝑥𝜓
3 cbvabv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
41, 2, 3cbvab 2728 1 {𝑥𝜑} = {𝑦𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  {cab 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598
This theorem is referenced by:  cdeqab1  3389  difjust  3537  unjust  3539  injust  3541  uniiunlem  3648  dfif3  4045  pwjust  4104  snjust  4119  intab  4432  intabs  4743  iotajust  5749  wfrlem1  7274  sbth  7938  cardprc  8662  iunfictbso  8793  aceq3lem  8799  isf33lem  9044  axdc3  9132  axdclem  9197  axdc  9199  genpv  9673  ltexpri  9717  recexpr  9725  supsr  9785  hashf1lem2  13045  cvbtrcl  13521  mertens  14399  4sq  15448  nbgraf1olem5  25736  dispcmp  29056  eulerpart  29573  ballotlemfmpn  29685  bnj66  29986  bnj1234  30137  subfacp1lem6  30223  subfacp1  30224  dfon2lem3  30736  dfon2lem7  30740  frrlem1  30826  f1omptsn  32159  ismblfin  32419  glbconxN  33481  eldioph3  36146  diophrex  36156  cbvcllem  36733  ssfiunibd  38263  isuhgr  40280  isushgr  40281  isupgr  40308  isumgr  40318  isuspgr  40380  isusgr  40381  isconngr  41354  isconngr1  41355  isfrgr  41428
  Copyright terms: Public domain W3C validator