Theorem cbvexv 1965

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

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

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  eujust  2079  euind  2990  reuind  3008  r19.2m  3578  r19.3rm  3580  r19.9rmv  3583  raaanlem  3596  raaan  3597  cbvopab2v  4161  bm1.3ii  4205  mss  4312  zfun  4525  xpiindim  4859  relop  4872  reldmm  4942  dmmrnm  4943  dmxpm  4944  dmcoss  4994  xpm  5150  cnviinm  5270  iotam  5310  fv3  5652  elfvm  5662  fo1stresm  6313  fo2ndresm  6314  tfr1onlemaccex  6500  tfrcllemaccex  6513  iinerm  6762  riinerm  6763  ixpiinm  6879  ac6sfi  7068  ctmlemr  7286  ctm  7287  ctssdclemr  7290  ctssdc  7291  fodjum  7324  finacn  7397  acfun  7400  ccfunen  7461  cc2lem  7463  cc2  7464  ltexprlemdisj  7804  ltexprlemloc  7805  recexprlemdisj  7828  suplocsr  8007  axpre-suploc  8100  nninfdcex  10469  zsupssdc  10470  zfz1isolem1  11075  climmo  11824  summodc  11909  nninfct  12577  ctiunct  13026  ismnd  13467  dfgrp3me  13648  issubg2m  13741  subrgintm  14222  islssm  14336  islidlm  14458  neipsm  14843  suplociccex  15314  bdbm1.3ii  16309