Theorem cbvexv 1310

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 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	cbvex 1162	1 |- (E.xph <-> E.yps)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953  E.wex 977

This theorem is referenced by:  cbvopab2v 2667  bm1.3ii 2696  axun 2858  relop 3265  fv3 3718  exfo 3807  rdglem2 3923  abfii4 4538  fodomfi 4540  aceq1 4701  aceq0 4702  aceq3lem 4704  aceq4 4706  axac 4717  kmlem2 4738  kmlem13 4749  zfcndun 4939  zfcndac 4943  sup2 5998  iserzext 7071  infxpidmlem2 7496  subbas 7586  infi1 10347  ficli 10368

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  df-ex 978

Copyright terms: Public domain