Theorem cbvabv 1905

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

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954  {cab 1461

This theorem is referenced by:  abidhb 1908  hbsbc1gd 1979  hbsbcgd 1980  uniiunlem 2128  intab 2555  intabs 2728  sbth 4443  abfii4 4544  aceq3lem 4712  zorn2 4776  genpv 5082  ltexpri 5129  recexpr 5140  suppsr2 5203  supsrlem4 5208  supsrlem6 5210  supsr 5211  pre-axsup 5271  infmap2lem1 7529  minvecex 8522  efghgrpilem 8653  ch2 9053

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain