Theorem cbvrabv 2422

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 1317	. 2 |- (z e. A -> A.x z e. A)
2		ax-17 1317	. 2 |- (z e. A -> A.y z e. A)
3		ax-17 1317	. 2 |- (ph -> A.yph)
4		ax-17 1317	. 2 |- (ps -> A.xps)
5		cbvrabv.1	. 2 |- (x = y -> (ph <-> ps))
6	1, 2, 3, 4, 5	cbvrab 2421	1 |- {x e. A | ph} = {y e. A | ps}

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   e. wcel 1300  {crab 2108

This theorem is referenced by:  reuuni3 3812  ordtype 5691  onsdom 5694  inf3lema 5715  omsubsuc 5877  zorn2 5958  uzwo3lem2 7430  sqrlem24 7946  sqrgt0ii 7947  sqrlem26 7948  seq1ubi 8164  acdc3 8755  acdc2 8759  acdc5 8762  acdc 8764  pilem3 10022  pilem4 10023  nmcopexi 11594  nmcfnexi 11623  cnlnadji 11646  nmopadjlei 11658  suprzcl 13658  divalglem5 13700  gcdcllem3 13720  ordtypeOLD 15382  onsdomOLD 15385  omsubsucOLD 15386

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-11 1309  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  df-clel 1880  df-rab 2112

Copyright terms: Public domain