Theorem cbval 2114

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 212	. . 3 |- ( x = y -> ( ph -> ps ) )
5	1, 2, 4	cbv3 2108	. 2 |- ( A. x ph -> A. y ps )
6	3	biimprd 231	. . . 4 |- ( x = y -> ( ps -> ph ) )
7	6	equcoms 1867	. . 3 |- ( y = x -> ( ps -> ph ) )
8	2, 1, 7	cbv3 2108	. 2 |- ( A. y ps -> A. x ph )
9	5, 8	impbii 192	1 |- ( A. x ph <-> A. y ps )

Syntax hints:   -> wi 4   <-> wb 189   A.wal 1445   F/wnf 1670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091

This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1667  df-nf 1671

This theorem is referenced by:  cbvex  2115  cbvalv  2116  cbval2  2120  sb8  2253  sb8eu  2332  cbvralf  2980  ralab2  3170  cbvralcsf  3362  dfss2f  3390  elintab  4214  reusv2lem4  4579  cbviota  5529  sb8iota  5531  dffun6f  5574  findcard2  7797  aceq1  8534  bnj1385  29649  bnj1476  29663  sbcalf  32353  alrimii  32360  aomclem6  35918  rababg  36180  dfcleqf  37426  stoweidlem34  37951