Theorem cbvabv 1900

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

Hypothesis

Ref	Expression
cbvabv.1	|- (x = y -> (ph <-> ps))

Assertion

Ref	Expression
cbvabv	|- {x | ph} = {y | ps}

Distinct variable groups:   x,y   ph,y   ps,x

Proof of Theorem cbvabv

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ph -> A.yph)
2		ax-17 968	. 2 |- (ps -> A.xps)
3		cbvabv.1	. 2 |- (x = y -> (ph <-> ps))
4	1, 2, 3	cbvab 1899	1 |- {x | ph} = {y | ps}

Syntax hints:   -> wi 3   <-> wb 146   = wceq 953  {cab 1456

This theorem is referenced by:  abidhb 1903  hbsbc1gd 1973  hbsbcgd 1974  uniiunlem 2122  intab 2550  intabs 2723  sbth 4437  abfii4 4538  aceq3lem 4704  zorn2 4768  genpv 5074  ltexpri 5121  recexpr 5132  suppsr2 5195  supsrlem4 5200  supsrlem6 5202  supsr 5203  pre-axsup 5263  infmap2lem1 7521  minvecex 8509  efghgrpilem 8634  ch2 9035

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-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803

Copyright terms: Public domain