Theorem cbvald 2025

Description: Deduction used to change bound variables, using implicit substitution, particularly useful in conjunction with dvelim 2079. (Contributed by NM, 2-Jan-2002.) (Revised by Mario Carneiro, 6-Oct-2016.) (Revised by Wolf Lammen, 13-May-2018.)

Hypotheses

Ref	Expression
cbvald.1
cbvald.2
cbvald.3

Assertion

Ref	Expression
cbvald

Distinct variable groups:   ,   ,

Proof of Theorem cbvald

Step	Hyp	Ref	Expression
1		nfv 1707	. 2
2		cbvald.1	. 2
3		cbvald.2	. 2
4		nfvd 1708	. 2
5		cbvald.3	. 2
6	1, 2, 3, 4, 5	cbv2 2020	1

Syntax hints:  ->wi 4  <->wb 184  A.wal 1393  F/wnf 1616

This theorem is referenced by:  cbvexd  2026  cbvaldva  2032  axextnd  8987  axrepndlem1  8988  axunndlem1  8991  axpowndlem2  8994  axpowndlem2OLD  8995  axpowndlem3  8996  axpowndlem3OLD  8997  axpowndlem4  8998  axregndlem2  9001  axregnd  9002  axregndOLD  9003  axinfnd  9005  axacndlem5  9010  axacnd  9011  axextdist  29232  distel  29236  wl-sb8eut  30022

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