Theorem cbvexv 1933

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2047  euind  2951  reuind  2969  r19.2m  3537  r19.3rm  3539  r19.9rmv  3542  raaanlem  3555  raaan  3556  cbvopab2v  4110  bm1.3ii  4154  mss  4259  zfun  4469  xpiindim  4803  relop  4816  dmmrnm  4885  dmxpm  4886  dmcoss  4935  xpm  5091  cnviinm  5211  iotam  5250  fv3  5581  elfvm  5591  fo1stresm  6219  fo2ndresm  6220  tfr1onlemaccex  6406  tfrcllemaccex  6419  iinerm  6666  riinerm  6667  ixpiinm  6783  ac6sfi  6959  ctmlemr  7174  ctm  7175  ctssdclemr  7178  ctssdc  7179  fodjum  7212  acfun  7274  ccfunen  7331  cc2lem  7333  cc2  7334  ltexprlemdisj  7673  ltexprlemloc  7674  recexprlemdisj  7697  suplocsr  7876  axpre-suploc  7969  nninfdcex  10327  zsupssdc  10328  zfz1isolem1  10932  climmo  11463  summodc  11548  nninfct  12208  ctiunct  12657  ismnd  13060  dfgrp3me  13232  issubg2m  13319  subrgintm  13799  islssm  13913  islidlm  14035  neipsm  14390  suplociccex  14861  bdbm1.3ii  15537