Theorem cbvex 1165

Description: Rule used to change bound variables with implicit substitution.

Hypotheses

Ref	Expression
cbvex.1	|- (ph -> A.yph)
cbvex.2	|- (ps -> A.xps)
cbvex.3	|- (x = y -> (ph <-> ps))

Assertion

Ref	Expression
cbvex	|- (E.xph <-> E.yps)

Proof of Theorem cbvex

Step	Hyp	Ref	Expression
1		cbvex.1	. . . . 5 |- (ph -> A.yph)
2	1	hbn 1003	. . . 4 |- (-. ph -> A.y -. ph)
3		cbvex.2	. . . . 5 |- (ps -> A.xps)
4	3	hbn 1003	. . . 4 |- (-. ps -> A.x -. ps)
5		cbvex.3	. . . . 5 |- (x = y -> (ph <-> ps))
6	5	negbid 610	. . . 4 |- (x = y -> (-. ph <-> -. ps))
7	2, 4, 6	cbval 1164	. . 3 |- (A.x -. ph <-> A.y -. ps)
8	7	negbii 187	. 2 |- (-. A.x -. ph <-> -. A.y -. ps)
9		df-ex 980	. 2 |- (E.xph <-> -. A.x -. ph)
10		df-ex 980	. 2 |- (E.yps <-> -. A.y -. ps)
11	8, 9, 10	3bitr4 183	1 |- (E.xph <-> E.yps)

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146  A.wal 953   = wceq 955  E.wex 979

This theorem is referenced by:  cbvexv 1314  cbvex2 1316  sb7f 1340  euf 1383  mo 1392  cbvmo 1407  mopick 1432  clelab 1579  cbvrex 1796  vtoclgf 1843  cla4gf 1857  eqvincf 1881  abn0 2287  eusn 2443  eluniab 2509  cbvopab1 2670  cbvopab1s 2671  axrep1 2690  axrep2 2691  axrep4 2693  opabid 2806  reusn 2888  dfdmf 3302  dfrnf 3344  zfcndrep 4949  nnwof 6404  cbvrexf 10396

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-12 967  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980

Copyright terms: Public domain