Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbvexv Unicode version

Theorem cbvexv 2024
 Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-1993.)
Hypothesis
Ref Expression
cbvalv.1
Assertion
Ref Expression
cbvexv
Distinct variable groups:   ,   ,

Proof of Theorem cbvexv
StepHypRef Expression
1 nfv 1707 . 2
2 nfv 1707 . 2
3 cbvalv.1 . 2
41, 2, 3cbvex 2022 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  E.wex 1612 This theorem is referenced by:  eujust  2284  euind  3286  reuind  3303  cbvopab2v  4526  bm1.3ii  4576  reusv2lem2  4654  relop  5158  dmcoss  5267  fv3  5884  exfo  6049  zfun  6593  ac6sfi  7784  brwdom2  8020  aceq1  8519  aceq0  8520  aceq3lem  8522  dfac4  8524  kmlem2  8552  kmlem13  8563  axdc4lem  8856  zfac  8861  zfcndun  9014  zfcndac  9018  sup2  10524  supmul  10536  climmo  13380  summo  13539  prodmo  13743  gsumval3eu  16907  elpt  20073  usgraedg4  24387  wfrlem1  29343  frrlem1  29387  fdc  30238  axc11next  31313  fnchoice  31404  bnj1185  33852 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999 This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617
 Copyright terms: Public domain W3C validator