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  4160  bm1.3ii  4204  mss  4311  zfun  4524  xpiindim  4858  relop  4871  reldmm  4941  dmmrnm  4942  dmxpm  4943  dmcoss  4993  xpm  5149  cnviinm  5269  iotam  5309  fv3  5649  elfvm  5659  fo1stresm  6305  fo2ndresm  6306  tfr1onlemaccex  6492  tfrcllemaccex  6505  iinerm  6752  riinerm  6753  ixpiinm  6869  ac6sfi  7056  ctmlemr  7271  ctm  7272  ctssdclemr  7275  ctssdc  7276  fodjum  7309  finacn  7382  acfun  7385  ccfunen  7446  cc2lem  7448  cc2  7449  ltexprlemdisj  7789  ltexprlemloc  7790  recexprlemdisj  7813  suplocsr  7992  axpre-suploc  8085  nninfdcex  10452  zsupssdc  10453  zfz1isolem1  11057  climmo  11804  summodc  11889  nninfct  12557  ctiunct  13006  ismnd  13447  dfgrp3me  13628  issubg2m  13721  subrgintm  14201  islssm  14315  islidlm  14437  neipsm  14822  suplociccex  15293  bdbm1.3ii  16212