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  4479  xpiindim  4813  relop  4826  dmmrnm  4895  dmxpm  4896  dmcoss  4945  xpm  5101  cnviinm  5221  iotam  5260  fv3  5593  elfvm  5603  fo1stresm  6237  fo2ndresm  6238  tfr1onlemaccex  6424  tfrcllemaccex  6437  iinerm  6684  riinerm  6685  ixpiinm  6801  ac6sfi  6977  ctmlemr  7192  ctm  7193  ctssdclemr  7196  ctssdc  7197  fodjum  7230  finacn  7298  acfun  7301  ccfunen  7358  cc2lem  7360  cc2  7361  ltexprlemdisj  7701  ltexprlemloc  7702  recexprlemdisj  7725  suplocsr  7904  axpre-suploc  7997  nninfdcex  10361  zsupssdc  10362  zfz1isolem1  10966  climmo  11528  summodc  11613  nninfct  12281  ctiunct  12730  ismnd  13169  dfgrp3me  13350  issubg2m  13443  subrgintm  13923  islssm  14037  islidlm  14159  neipsm  14544  suplociccex  15015  bdbm1.3ii  15691