Theorem cbvex 2272

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

Hypotheses

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

Assertion

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

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbval.1	. . . . 5 |- F/ y ph
2	1	nfn 1784	. . . 4 |- F/ y -. ph
3		cbval.2	. . . . 5 |- F/ x ps
4	3	nfn 1784	. . . 4 |- F/ x -. ps
5		cbval.3	. . . . 5 |- ( x = y -> ( ph <-> ps ) )
6	5	notbid 308	. . . 4 |- ( x = y -> ( -. ph <-> -. ps ) )
7	2, 4, 6	cbval 2271	. . 3 |- ( A. x -. ph <-> A. y -. ps )
8	7	notbii 310	. 2 |- ( -. A. x -. ph <-> -. A. y -. ps )
9		df-ex 1705	. 2 |- ( E. x ph <-> -. A. x -. ph )
10		df-ex 1705	. 2 |- ( E. y ps <-> -. A. y -. ps )
11	8, 9, 10	3bitr4i 292	1 |- ( E. x ph <-> E. y ps )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   A.wal 1481   E.wex 1704   F/wnf 1708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  cbvexvOLD  2276  sb8e  2425  exsb  2468  euf  2478  mo2  2479  cbvmo  2506  clelab  2748  issetf  3208  eqvincf  3331  rexab2  3373  euabsn  4261  eluniab  4447  cbvopab1  4723  cbvopab2  4724  cbvopab1s  4725  axrep1  4772  axrep2  4773  axrep4  4775  opeliunxp  5170  dfdmf  5317  dfrnf  5364  elrnmpt1  5374  cbvoprab1  6727  cbvoprab2  6728  opabex3d  7145  opabex3  7146  zfcndrep  9436  fsum2dlem  14501  fprod2dlem  14710  bnj1146  30862  bnj607  30986  bnj1228  31079  poimirlem26  33435  sbcexf  33918  elunif  39175  stoweidlem46  40263  opeliun2xp  42111