Theorem cbval 2026

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 2020	. 2 |- ( A. x ph -> A. y ps )
6	3	biimprd 223	. . . 4 |- ( x = y -> ( ps -> ph ) )
7	6	equcoms 1800	. . 3 |- ( y = x -> ( ps -> ph ) )
8	2, 1, 7	cbv3 2020	. 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 1396   F/wnf 1621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622

This theorem is referenced by:  cbvex  2027  cbvalv  2028  cbval2  2032  sb8  2169  sb8eu  2319  sb8euOLD  2320  cleqh  2569  abbiOLD  2586  cleqfOLD  2644  cbvralf  3075  ralab2  3261  cbvralcsf  3452  dfss2f  3480  elintab  4282  reusv2lem4  4641  cbviota  5539  sb8iota  5541  dffun6f  5584  findcard2  7752  aceq1  8489  sbcalf  30757  alrimii  30764  aomclem6  31244  stoweidlem34  32055  bnj1385  34292  bnj1476  34306