Theorem cbvabv 1909

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 971	. 2 |- (ph -> A.yph)
2		ax-17 971	. 2 |- (ps -> A.xps)
3		cbvabv.1	. 2 |- (x = y -> (ph <-> ps))
4	1, 2, 3	cbvab 1908	1 |- {x | ph} = {y | ps}

Syntax hints:   -> wi 3   <-> wb 146   = wceq 956  {cab 1463

This theorem is referenced by:  abidhb 1912  hbsbc1gd 1983  hbsbcgd 1984  uniiunlem 2132  intab 2560  intabs 2733  sbth 4457  abfii4OLD 4564  aceq3lem 4732  zorn2 4796  genpv 5102  ltexpri 5149  recexpr 5160  suppsr2 5223  supsrlem4 5228  supsrlem6 5230  supsr 5231  pre-axsup 5291  infmap2lem1 7579  minvecex 8578  efghgrpilem 8719  ch2 9114

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-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain