Theorem cbval 1161

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

Hypotheses

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

Assertion

Ref	Expression
cbval	|- (A.xph <-> A.yps)

Proof of Theorem cbval

Step	Hyp	Ref	Expression
1		cbval.1	. . . 4 |- (ph -> A.yph)
2	1	imim2i 17	. . 3 |- ((ph -> ph) -> (ph -> A.yph))
3		cbval.2	. . . 4 |- (ps -> A.xps)
4	3	a1i 8	. . 3 |- ((ph -> ph) -> (ps -> A.xps))
5		cbval.3	. . . 4 |- (x = y -> (ph <-> ps))
6	5	a1i 8	. . 3 |- ((ph -> ph) -> (x = y -> (ph <-> ps)))
7	2, 4, 6	cbv2 1159	. 2 |- (A.xA.y(ph -> ph) -> (A.xph <-> A.yps))
8		id 59	. . 3 |- (ph -> ph)
9	8	ax-gen 960	. 2 |- A.y(ph -> ph)
10	7, 9	mpg 983	1 |- (A.xph <-> A.yps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 951   = wceq 953

This theorem is referenced by:  cbvex 1162  cbvalv 1309  cbval2 1311  cbvald 1315  cleqf 1552  cbvralf 1788  dfss2f 2050  elintab 2534  ssintab 2540  dffunmof 3516  aceq1 4701  nnwof 6391  homcard 10426

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119

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

Copyright terms: Public domain