Theorem cbval 1768

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

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

This theorem is referenced by:  sb8  1870  cbval2  1936  sb8eu  2058  abbi  2310  cleqf  2364  cbvralf  2721  ralab2  2928  cbvralcsf  3147  dfss2f  3175  elintab  3886  cbviota  5225  sb8iota  5227  dffun6f  5272  dffun4f  5275  mptfvex  5650  findcard2  6959  findcard2s  6960