Theorem cbvalv 1312

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

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

This theorem is referenced by:  axpow 2738  pssnn 4519  unifi 4538  fodomfi 4546  axinf 4603  aceq0 4710  aceq3 4713  aceq5 4720  axac 4725  kmlem1 4745  kmlem13 4757  zfcndpow 4948  zfcndinf 4950  zfcndac 4951  axgroth4 8719

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121

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

Copyright terms: Public domain