Theorem cbvexv 1315

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

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956  E.wex 980

This theorem is referenced by:  cbvopab2v 2675  bm1.3ii 2704  axun 2865  relop 3273  fv3 3731  exfo 3820  rdglem2 3936  abfii4 4552  fodomfi 4554  aceq1 4717  aceq0 4718  aceq3lem 4720  aceq4 4722  axac 4733  kmlem2 4754  kmlem13 4765  zfcndun 4955  zfcndac 4959  sup2 6019  iserzext 7093  infxpidmlem2 7510  subbas 7601  infi1 10401  ficli 10422  rcfpfillem4 10510  rcfpfillem6 10512

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

Copyright terms: Public domain