Theorem cbval 1969

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 13-May-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		cbval.2	. . 3 |- F/ x ps
3		cbval.3	. . . 4 |- ( x = y -> ( ph <-> ps ) )
4	3	biimpd 207	. . 3 |- ( x = y -> ( ph -> ps ) )
5	1, 2, 4	cbv3 1959	. 2 |- ( A. x ph -> A. y ps )
6	3	biimprd 223	. . . 4 |- ( x = y -> ( ps -> ph ) )
7	6	equcoms 1733	. . 3 |- ( y = x -> ( ps -> ph ) )
8	2, 1, 7	cbv3 1959	. 2 |- ( A. y ps -> A. x ph )
9	5, 8	impbii 188	1 |- ( A. x ph <-> A. y ps )

Syntax hints:   -> wi 4   <-> wb 184   A.wal 1367   F/wnf 1589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590

This theorem is referenced by:  cbvex  1970  cbvalv  1971  cbval2  1975  sb8  2124  sb8eu  2292  sb8euOLD  2293  sb8euOLDOLD  2294  abbi  2551  cleqf  2601  cbvralf  2939  ralab2  3122  cbvralcsf  3317  dfss2f  3345  elintab  4137  reusv2lem4  4494  cbviota  5384  sb8iota  5386  dffun6f  5430  findcard2  7550  aceq1  8285  sbcalf  28917  alrimii  28924  aomclem6  29409  stoweidlem34  29826  bnj1385  31823  bnj1476  31837