Theorem cbvalv 2273

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.) Remove dependency on ax-10 2019. (Revised by Wolf Lammen, 17-Jul-2021.)

Hypothesis

Ref	Expression
cbvalv.1	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
cbvalv	|- ( A. x ph <-> A. y ps )

Distinct variable groups:   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem cbvalv

Step	Hyp	Ref	Expression
1		ax-5 1839	. . . 4 |- ( ph -> A. y ph )
2	1	hbal 2036	. . 3 |- ( A. x ph -> A. y A. x ph )
3		cbvalv.1	. . . 4 |- ( x = y -> ( ph <-> ps ) )
4	3	spv 2260	. . 3 |- ( A. x ph -> ps )
5	2, 4	alrimih 1751	. 2 |- ( A. x ph -> A. y ps )
6		ax-5 1839	. . . 4 |- ( ps -> A. x ps )
7	6	hbal 2036	. . 3 |- ( A. y ps -> A. x A. y ps )
8	3	equcoms 1947	. . . . 5 |- ( y = x -> ( ph <-> ps ) )
9	8	bicomd 213	. . . 4 |- ( y = x -> ( ps <-> ph ) )
10	9	spv 2260	. . 3 |- ( A. y ps -> ph )
11	7, 10	alrimih 1751	. 2 |- ( A. y ps -> A. x ph )
12	5, 11	impbii 199	1 |- ( A. x ph <-> A. y ps )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481

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-11 2034  ax-12 2047  ax-13 2246

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

This theorem is referenced by:  cbvexv  2275  cbvaldva  2281  cbval2v  2285  nfcjust  2752  cdeqal1  3426  zfpow  4844  tfisi  7058  pssnn  8178  findcard  8199  findcard3  8203  zfinf  8536  aceq0  8941  kmlem1  8972  kmlem13  8984  fin23lem32  9166  fin23lem41  9174  zfac  9282  zfcndpow  9438  zfcndinf  9440  zfcndac  9441  axgroth4  9654  relexpindlem  13803  ramcl  15733  mreexexlemd  16304  bnj1112  31051  dfon2lem6  31693  dfon2lem7  31694  dfon2  31697  phpreu  33393  axc11n-16  34223  dfac11  37632