Theorem cbvex 1804

Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
cbvex.1	|- F/ y ph
cbvex.2	|- F/ x ps
cbvex.3	|- ( x = y -> ( ph <-> ps ) )

Assertion

Ref	Expression
cbvex	|- ( E. x ph <-> E. y ps )

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbvex.1	. . 3 |- F/ y ph
2	1	nfri 1568	. 2 |- ( ph -> A. y ph )
3		cbvex.2	. . 3 |- F/ x ps
4	3	nfri 1568	. 2 |- ( ps -> A. x ps )
5		cbvex.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	2, 4, 5	cbvexh 1803	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1509   E.wex 1541

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510

This theorem is referenced by:  sb8e  1905  cbvex2  1971  cbvmo  2119  mo23  2121  clelab  2358  cbvrexf  2760  issetf  2811  eqvincf  2932  rexab2  2973  cbvrexcsf  3192  abn0m  3522  rabn0m  3524  euabsn  3745  eluniab  3910  cbvopab1  4167  cbvopab2  4168  cbvopab1s  4169  intexabim  4247  iinexgm  4249  opeliunxp  4787  dfdmf  4930  dfrnf  4979  elrnmpt1  4989  cbvoprab1  6103  cbvoprab2  6104  opabex3d  6292  opabex3  6293  seq3f1olemp  10823  fsum2dlemstep  12058  bdsepnfALT  16588  strcollnfALT  16685