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

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		nfv 1707	. 2
3		cbvalv.1	. 2
4	1, 2, 3	cbvex 2022	1

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