Theorem cbval 1742

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 1507	. 2 |- ( ph -> A. y ph )
3		cbval.2	. . 3 |- F/ x ps
4	3	nfri 1507	. 2 |- ( ps -> A. x ps )
5		cbval.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	2, 4, 5	cbvalh 1741	1 |- ( A. x ph <-> A. y ps )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1341   F/wnf 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  sb8  1844  cbval2  1909  sb8eu  2027  abbi  2280  cleqf  2333  cbvralf  2685  ralab2  2890  cbvralcsf  3107  dfss2f  3133  elintab  3835  cbviota  5158  sb8iota  5160  dffun6f  5201  dffun4f  5204  mptfvex  5571  findcard2  6855  findcard2s  6856