Theorem cbval 1637

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

Syntax hints:   -> wi 4   <-> wb 98   A.wal 1241   F/wnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  sb8  1736  cbval2  1796  sb8eu  1913  abbi  2151  cleqf  2201  cbvralf  2527  ralab2  2705  cbvralcsf  2908  dfss2f  2936  elintab  3626  cbviota  4872  sb8iota  4874  dffun6f  4915  dffun4f  4918  mptfvex  5256  findcard2  6346  findcard2s  6347