Theorem cbvrabv 1907

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution.

Hypothesis

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

Assertion

Ref	Expression
cbvrabv	|- {x e. A | ph} = {y e. A | ps}

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

Proof of Theorem cbvrabv

Step	Hyp	Ref	Expression
1		ax-17 969	. 2 |- (z e. A -> A.x z e. A)
2		ax-17 969	. 2 |- (z e. A -> A.y z e. A)
3		ax-17 969	. 2 |- (ph -> A.yph)
4		ax-17 969	. 2 |- (ps -> A.xps)
5		cbvrabv.1	. 2 |- (x = y -> (ph <-> ps))
6	1, 2, 3, 4, 5	cbvrab 1906	1 |- {x e. A | ph} = {y e. A | ps}

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956  {crab 1645

This theorem is referenced by:  reuuni3 2881  inf3lema 4589  zorn2 4776  uzwo3lem2 6173  sqrlem24 6634  sqrgt0i 6635  sqrlem26 6636  seq1ub 6857  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  pilem3 8611  pilem4 8612  nmcopex 9895  nmcfnex 9924  cnlnadj 9947  nmopadjle 9959

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-rab 1649  df-v 1808

Copyright terms: Public domain