Theorem cbval 1802

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 3-Oct-2016.)

Hypotheses

Ref	Expression
cbval.1	|- F/ y ph
cbval.2	|- F/ x ps
cbval.3	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
cbval	|- ( A. x ph <-> A. y ps )

Proof of Theorem cbval

Step	Hyp	Ref	Expression
1		cbval.1	. . 3 |- F/ y ph
2	1	nfri 1568	. 2 |- ( ph -> A. y ph )
3		cbval.2	. . 3 |- F/ x ps
4	3	nfri 1568	. 2 |- ( ps -> A. x ps )
5		cbval.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	2, 4, 5	cbvalh 1801	1 |- ( A. x ph <-> A. y ps )

Syntax hints:   -> wi 4   <-> wb 105   A.wal 1396   F/wnf 1509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510

This theorem is referenced by:  sb8  1904  cbval2  1970  sb8eu  2092  abbi  2345  cleqf  2400  cbvralf  2759  ralab2  2971  cbvralcsf  3191  dfss2f  3219  elintab  3944  cbviota  5298  sb8iota  5301  dffun6f  5346  dffun4f  5349  mptfvex  5741  findcard2  7121  findcard2s  7122