Theorem cbvrab 3032

Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by Andrew Salmon, 11-Jul-2011.) (Revised by Mario Carneiro, 9-Oct-2016.)

Hypotheses

Ref	Expression
cbvrab.1	|- F/_ x A
cbvrab.2	|- F/_ y A
cbvrab.3	|- F/ y ph
cbvrab.4	|- F/ x ps
cbvrab.5	|- ( x = y -> ( ph <-> ps ) )

Assertion

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

Proof of Theorem cbvrab

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1715	. . . 4 |- F/ z ( x e. A /\ ph )
2		cbvrab.1	. . . . . 6 |- F/_ x A
3	2	nfcri 2537	. . . . 5 |- F/ x z e. A
4		nfs1v 2185	. . . . 5 |- F/ x [ z / x ] ph
5	3, 4	nfan 1936	. . . 4 |- F/ x ( z e. A /\ [ z / x ] ph )
6		eleq1 2454	. . . . 5 |- ( x = z -> ( x e. A <-> z e. A ) )
7		sbequ12 2000	. . . . 5 |- ( x = z -> ( ph <-> [ z / x ] ph ) )
8	6, 7	anbi12d 708	. . . 4 |- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
9	1, 5, 8	cbvab 2523	. . 3 |- { x | ( x e. A /\ ph ) } = { z | ( z e. A /\ [ z / x ] ph ) }
10		cbvrab.2	. . . . . 6 |- F/_ y A
11	10	nfcri 2537	. . . . 5 |- F/ y z e. A
12		cbvrab.3	. . . . . 6 |- F/ y ph
13	12	nfsb 2188	. . . . 5 |- F/ y [ z / x ] ph
14	11, 13	nfan 1936	. . . 4 |- F/ y ( z e. A /\ [ z / x ] ph )
15		nfv 1715	. . . 4 |- F/ z ( y e. A /\ ps )
16		eleq1 2454	. . . . 5 |- ( z = y -> ( z e. A <-> y e. A ) )
17		sbequ 2121	. . . . . 6 |- ( z = y -> ( [ z / x ] ph <-> [ y / x ] ph ) )
18		cbvrab.4	. . . . . . 7 |- F/ x ps
19		cbvrab.5	. . . . . . 7 |- ( x = y -> ( ph <-> ps ) )
20	18, 19	sbie 2153	. . . . . 6 |- ( [ y / x ] ph <-> ps )
21	17, 20	syl6bb 261	. . . . 5 |- ( z = y -> ( [ z / x ] ph <-> ps ) )
22	16, 21	anbi12d 708	. . . 4 |- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
23	14, 15, 22	cbvab 2523	. . 3 |- { z | ( z e. A /\ [ z / x ] ph ) } = { y | ( y e. A /\ ps ) }
24	9, 23	eqtri 2411	. 2 |- { x | ( x e. A /\ ph ) } = { y | ( y e. A /\ ps ) }
25		df-rab 2741	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
26		df-rab 2741	. 2 |- { y e. A | ps } = { y | ( y e. A /\ ps ) }
27	24, 25, 26	3eqtr4i 2421	1 |- { x e. A | ph } = { y e. A | ps }

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 367   = wceq 1399   F/wnf 1624   [wsb 1747   e. wcel 1826   {cab 2367   F/_wnfc 2530   {crab 2736

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741

This theorem is referenced by:  cbvrabv  3033  elrabsf  3291  tfis  6588  cantnflem1  8021  scottexs  8218  scott0s  8219  elmptrab  20413  suppss2f  27617  scottexf  30742  scott0f  30743  eq0rabdioph  30875  rexrabdioph  30893  rexfrabdioph  30894  elnn0rabdioph  30902  dvdsrabdioph  30909  binomcxplemdvsum  31428  stoweidlem34  31982  stoweidlem59  32007  bnj1534  34258