Theorem cbval 2271

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 219	. . 3 |- ( x = y -> ( ph -> ps ) )
5	1, 2, 4	cbv3 2265	. 2 |- ( A. x ph -> A. y ps )
6	3	biimprd 238	. . . 4 |- ( x = y -> ( ps -> ph ) )
7	6	equcoms 1947	. . 3 |- ( y = x -> ( ps -> ph ) )
8	2, 1, 7	cbv3 2265	. 2 |- ( A. y ps -> A. x ph )
9	5, 8	impbii 199	1 |- ( A. x ph <-> A. y ps )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  cbvex  2272  cbvalvOLD  2274  cbval2  2279  sb8  2424  sb8eu  2503  cbvralf  3165  ralab2  3371  cbvralcsf  3565  dfss2f  3594  elintab  4487  reusv2lem4  4872  cbviota  5856  sb8iota  5858  dffun6f  5902  findcard2  8200  aceq1  8940  bnj1385  30903  sbcalf  33917  alrimii  33924  aomclem6  37629  rababg  37879