Theorem cbval 1165

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 1163	. 2 |- (A.xA.y(ph -> ph) -> (A.xph <-> A.yps))
8		id 59	. . 3 |- (ph -> ph)
9	8	ax-gen 963	. 2 |- A.y(ph -> ph)
10	7, 9	mpg 986	1 |- (A.xph <-> A.yps)

Syntax hints:   -> wi 3   <-> wb 146  A.wal 954   = wceq 956

This theorem is referenced by:  cbvex 1166  cbvalv 1314  cbval2 1316  cbvald 1320  cleqf 1560  cbvralf 1796  dfss2f 2060  elintab 2544  ssintab 2550  dffunmof 3530  aceq1 4729  nnwof 6459  homcard 10539

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-12 968  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123

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

Copyright terms: Public domain