Theorem cbvabv 2420

Description: Rule used to change bound variables, using implicit substitution.

Hypothesis

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

Assertion

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

Distinct variable groups:   ph,y   ps,x

Proof of Theorem cbvabv

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

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298  {cab 1871

This theorem is referenced by:  abidhb 2423  hbsbc1gdOLD 2516  hbsbcgdOLD 2518  difjust 2595  unjust 2598  injust 2601  uniiunlem 2693  pwjust 3033  snjust 3047  intab 3247  intabs 3469  euobj1 3834  iotajust 5088  sbth 5520  abfii4 5654  aceq3lem 5894  zorn2 5958  genpv 6254  ltexpri 6301  recexpr 6312  suppsr2 6375  supsrlem4 6380  supsrlem6 6382  supsr 6383  pre-axsup 6444  infmap2lem1 8848  minvecex 9923  efghgrpilem 10073  ch2 10747  bnj78 12439  bnj79OLD 12441  bnj100 12449  bnj99 12450  bnj1273 13029  bnj1234 13460  dfon2lem3 13851  dfon2lem7 13855  wfrlem1 13957  cntrset 15000  fictblem 15370  fictb 15371  neibastop2lem4 15522  stb2strx 16747  stb3strx 16754  glbconx 17029  isgrpiNEW 17115

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877

Copyright terms: Public domain