Theorem cbvex 1712

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

Syntax hints:   -> wi 4   <-> wb 104   F/wnf 1419   E.wex 1451

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497

This theorem depends on definitions:  df-bi 116  df-nf 1420

This theorem is referenced by:  sb8e  1811  cbvex2  1872  cbvmo  2015  mo23  2016  clelab  2239  cbvrexf  2623  issetf  2664  eqvincf  2780  rexab2  2819  cbvrexcsf  3029  abn0m  3354  rabn0m  3356  euabsn  3559  eluniab  3714  cbvopab1  3961  cbvopab2  3962  cbvopab1s  3963  intexabim  4037  iinexgm  4039  opeliunxp  4554  dfdmf  4692  dfrnf  4740  elrnmpt1  4750  cbvoprab1  5797  cbvoprab2  5798  opabex3d  5973  opabex3  5974  seq3f1olemp  10168  fsum2dlemstep  11095  bdsepnfALT  12779  strcollnfALT  12876