Theorem cbvalv 1309

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 groups:   ph,y   ps,x

Proof of Theorem cbvalv

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

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951   = wceq 953

This theorem is referenced by:  axpow 2733  pssnn 4513  unifi 4532  fodomfi 4540  axinf 4595  aceq0 4702  aceq3 4705  aceq5 4712  axac 4717  kmlem1 4737  kmlem13 4749  zfcndpow 4940  zfcndinf 4942  zfcndac 4943  axgroth4 8719

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain