Theorem cbvalv 972

Description: Rule used to change bound variables with implicit substitution.

Hypothesis

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

Assertion

Ref	Expression
cbvalv	|- (A.xph <-> A.yps)

Distinct variable group(s):   ph,y   ps,x

Proof of Theorem cbvalv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ph -> A.yph)
2		ax-17 925	. 2 |- (ps -> A.xps)
3		cbvalv.1	. 2 |- (x = y -> (ph <-> ps))
4	1, 2, 3	cbval 848	1 |- (A.xph <-> A.yps)

Syntax hints:   -> wi 2   <-> wb 127  A.wal 672   = weq 797

This theorem is referenced by:  axpow 1082  axinf 1084  axac 1085  pssnn 3428  inf0 3457  aceq0 3553  aceq3 3556  aceq5 3563  kmlem1 3580  kmlem12 3591  zfcndpow 3762  zfcndinf 3764  zfcndac 3765

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-12 802  ax-17 925

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679

metamath.org