Theorem cbvex 1770

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 1533	. 2 |- ( ph -> A. y ph )
3		cbvex.2	. . 3 |- F/ x ps
4	3	nfri 1533	. 2 |- ( ps -> A. x ps )
5		cbvex.3	. 2 |- ( x = y -> ( ph <-> ps ) )
6	2, 4, 5	cbvexh 1769	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -> wi 4   <-> wb 105   F/wnf 1474   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  df-nf 1475

This theorem is referenced by:  sb8e  1871  cbvex2  1937  cbvmo  2085  mo23  2086  clelab  2322  cbvrexf  2722  issetf  2770  eqvincf  2889  rexab2  2930  cbvrexcsf  3148  abn0m  3477  rabn0m  3479  euabsn  3693  eluniab  3852  cbvopab1  4107  cbvopab2  4108  cbvopab1s  4109  intexabim  4186  iinexgm  4188  opeliunxp  4719  dfdmf  4860  dfrnf  4908  elrnmpt1  4918  cbvoprab1  5998  cbvoprab2  5999  opabex3d  6187  opabex3  6188  seq3f1olemp  10624  fsum2dlemstep  11616  bdsepnfALT  15619  strcollnfALT  15716