Theorem cbvexv 1795

Description: Rule used to change bound variables, using implicit substitition. (Contributed by NM, 5-Aug-1993.)

Hypothesis

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

Assertion

Ref	Expression
cbvexv	|- ( E. x ph <-> E. y ps )

Distinct variable groups:   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem cbvexv

Step	Hyp	Ref	Expression
1		ax-17 1419	. 2 |- ( ph -> A. y ph )
2		ax-17 1419	. 2 |- ( ps -> A. x ps )
3		cbvalv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvexh 1638	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -> wi 4   <-> wb 98   E.wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  eujust  1902  euind  2728  reuind  2744  r19.3rm  3310  r19.9rmv  3313  raaanlem  3326  raaan  3327  cbvopab2v  3834  bm1.3ii  3878  mss  3962  zfun  4171  xpiindim  4473  relop  4486  dmmrnm  4554  dmxpm  4555  dmcoss  4601  xpm  4745  cnviinm  4859  fv3  5197  fo1stresm  5788  fo2ndresm  5789  iinerm  6178  riinerm  6179  ac6sfi  6352  ltexprlemdisj  6704  ltexprlemloc  6705  recexprlemdisj  6728  climmo  9819  bdbm1.3ii  10011