Theorem cbvex 1805

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 1804	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  1906  cbvex2  1974  cbvmo  2122  mo23  2124  clelab  2362  cbvrexf  2772  issetf  2823  eqvincf  2945  rexab2  2986  cbvrexcsf  3205  abn0m  3538  rabn0m  3540  euabsn  3766  eluniab  3931  cbvopab1  4188  cbvopab2  4189  cbvopab1s  4190  intexabim  4269  iinexgm  4271  opeliunxp  4810  dfdmf  4954  dfrnf  5003  elrnmpt1  5013  cbvoprab1  6133  cbvoprab2  6134  opabex3d  6323  opabex3  6324  seq3f1olemp  10901  fsum2dlemstep  12145  bdsepnfALT  16785  strcollnfALT  16882