Theorem cbvexv 1317

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

Hypothesis

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

Assertion

Ref	Expression
cbvexv	|- (E.xph <-> E.yps)

Distinct variable groups:   ph,y   ps,x

Proof of Theorem cbvexv

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

Syntax hints:   -> wi 3   <-> wb 146   = wceq 958  E.wex 982

This theorem is referenced by:  cbvopab2v 2682  bm1.3ii 2711  axun 2873  relop 3281  fv3 3739  exfo 3828  rdglem2 3944  fodomfi 4575  fodomfiOLD 4576  aceq1 4739  aceq0 4740  aceq3lem 4742  aceq4 4744  axac 4755  kmlem2 4776  kmlem13 4787  zfcndun 4979  zfcndac 4983  sup2 6053  iserzext 7135  infxpidmlem2 7554  infi1 10441  ficli 10462  rcfpfillem4 10566  rcfpfillem6 10568

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125

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

Copyright terms: Public domain