Theorem cbvexv 1930

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 1537	. 2 |- ( ph -> A. y ph )
2		ax-17 1537	. 2 |- ( ps -> A. x ps )
3		cbvalv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
4	1, 2, 3	cbvexh 1766	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -> wi 4   <-> wb 105   E.wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2044  euind  2947  reuind  2965  r19.2m  3533  r19.3rm  3535  r19.9rmv  3538  raaanlem  3551  raaan  3552  cbvopab2v  4106  bm1.3ii  4150  mss  4255  zfun  4465  xpiindim  4799  relop  4812  dmmrnm  4881  dmxpm  4882  dmcoss  4931  xpm  5087  cnviinm  5207  iotam  5246  fv3  5577  elfvm  5587  fo1stresm  6214  fo2ndresm  6215  tfr1onlemaccex  6401  tfrcllemaccex  6414  iinerm  6661  riinerm  6662  ixpiinm  6778  ac6sfi  6954  ctmlemr  7167  ctm  7168  ctssdclemr  7171  ctssdc  7172  fodjum  7205  acfun  7267  ccfunen  7324  cc2lem  7326  cc2  7327  ltexprlemdisj  7666  ltexprlemloc  7667  recexprlemdisj  7690  suplocsr  7869  axpre-suploc  7962  zfz1isolem1  10911  climmo  11441  summodc  11526  nninfdcex  12090  zsupssdc  12091  nninfct  12178  ctiunct  12597  ismnd  13000  dfgrp3me  13172  issubg2m  13259  subrgintm  13739  islssm  13853  islidlm  13975  neipsm  14322  suplociccex  14779  bdbm1.3ii  15383