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  2948  reuind  2966  r19.2m  3534  r19.3rm  3536  r19.9rmv  3539  raaanlem  3552  raaan  3553  cbvopab2v  4107  bm1.3ii  4151  mss  4256  zfun  4466  xpiindim  4800  relop  4813  dmmrnm  4882  dmxpm  4883  dmcoss  4932  xpm  5088  cnviinm  5208  iotam  5247  fv3  5578  elfvm  5588  fo1stresm  6216  fo2ndresm  6217  tfr1onlemaccex  6403  tfrcllemaccex  6416  iinerm  6663  riinerm  6664  ixpiinm  6780  ac6sfi  6956  ctmlemr  7169  ctm  7170  ctssdclemr  7173  ctssdc  7174  fodjum  7207  acfun  7269  ccfunen  7326  cc2lem  7328  cc2  7329  ltexprlemdisj  7668  ltexprlemloc  7669  recexprlemdisj  7692  suplocsr  7871  axpre-suploc  7964  zfz1isolem1  10914  climmo  11444  summodc  11529  nninfdcex  12093  zsupssdc  12094  nninfct  12181  ctiunct  12600  ismnd  13003  dfgrp3me  13175  issubg2m  13262  subrgintm  13742  islssm  13856  islidlm  13978  neipsm  14333  suplociccex  14804  bdbm1.3ii  15453