Theorem cbvalv 1314

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 971	. 2 |- (ph -> A.yph)
2		ax-17 971	. 2 |- (ps -> A.xps)
3		cbvalv.1	. 2 |- (x = y -> (ph <-> ps))
4	1, 2, 3	cbval 1165	1 |- (A.xph <-> A.yps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956

This theorem is referenced by:  axpow 2743  pssnn 4534  unifiOLD 4557  fodomfiOLD 4566  axinf 4623  aceq0 4730  aceq3 4733  aceq5 4740  axac 4745  kmlem1 4765  kmlem13 4777  zfcndpow 4968  zfcndinf 4970  zfcndac 4971  axgroth4 8780

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

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

Copyright terms: Public domain