Theorem cbvexv 1941

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

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

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2055  euind  2959  reuind  2977  r19.2m  3546  r19.3rm  3548  r19.9rmv  3551  raaanlem  3564  raaan  3565  cbvopab2v  4120  bm1.3ii  4164  mss  4269  zfun  4480  xpiindim  4814  relop  4827  dmmrnm  4896  dmxpm  4897  dmcoss  4947  xpm  5103  cnviinm  5223  iotam  5262  fv3  5598  elfvm  5608  fo1stresm  6246  fo2ndresm  6247  tfr1onlemaccex  6433  tfrcllemaccex  6446  iinerm  6693  riinerm  6694  ixpiinm  6810  ac6sfi  6994  ctmlemr  7209  ctm  7210  ctssdclemr  7213  ctssdc  7214  fodjum  7247  finacn  7315  acfun  7318  ccfunen  7375  cc2lem  7377  cc2  7378  ltexprlemdisj  7718  ltexprlemloc  7719  recexprlemdisj  7742  suplocsr  7921  axpre-suploc  8014  nninfdcex  10378  zsupssdc  10379  zfz1isolem1  10983  climmo  11551  summodc  11636  nninfct  12304  ctiunct  12753  ismnd  13193  dfgrp3me  13374  issubg2m  13467  subrgintm  13947  islssm  14061  islidlm  14183  neipsm  14568  suplociccex  15039  bdbm1.3ii  15760