Theorem cbval 1754

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534

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

This theorem is referenced by:  sb8  1856  cbval2  1921  sb8eu  2039  abbi  2291  cleqf  2344  cbvralf  2697  ralab2  2902  cbvralcsf  3120  dfss2f  3147  elintab  3856  cbviota  5184  sb8iota  5186  dffun6f  5230  dffun4f  5233  mptfvex  5602  findcard2  6889  findcard2s  6890