Theorem cbval 1987

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 1977	. 2 |- ( A. x ph -> A. y ps )
6	3	biimprd 223	. . . 4 |- ( x = y -> ( ps -> ph ) )
7	6	equcoms 1739	. . 3 |- ( y = x -> ( ps -> ph ) )
8	2, 1, 7	cbv3 1977	. 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 1372   F/wnf 1594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592  df-nf 1595

This theorem is referenced by:  cbvex  1988  cbvalv  1989  cbval2  1993  sb8  2140  sb8eu  2307  sb8euOLD  2308  sb8euOLDOLD  2309  cleqh  2575  abbiOLD  2592  cleqfOLD  2650  cbvralf  3075  ralab2  3261  cbvralcsf  3460  dfss2f  3488  elintab  4286  reusv2lem4  4644  cbviota  5547  sb8iota  5549  dffun6f  5593  findcard2  7749  aceq1  8487  sbcalf  30107  alrimii  30114  aomclem6  30598  stoweidlem34  31289  bnj1385  32845  bnj1476  32859