Theorem cbval 1800

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

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

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

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

This theorem is referenced by:  sb8  1902  cbval2  1968  sb8eu  2090  abbi  2343  cleqf  2397  cbvralf  2756  ralab2  2968  cbvralcsf  3188  dfss2f  3216  elintab  3937  cbviota  5289  sb8iota  5292  dffun6f  5337  dffun4f  5340  mptfvex  5728  findcard2  7071  findcard2s  7072