Theorem cbvrab 3042

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 1760	. . . 4 |- F/ z ( x e. A /\ ph )
2		cbvrab.1	. . . . . 6 |- F/_ x A
3	2	nfcri 2585	. . . . 5 |- F/ x z e. A
4		nfs1v 2265	. . . . 5 |- F/ x [ z / x ] ph
5	3, 4	nfan 2010	. . . 4 |- F/ x ( z e. A /\ [ z / x ] ph )
6		eleq1 2516	. . . . 5 |- ( x = z -> ( x e. A <-> z e. A ) )
7		sbequ12 2082	. . . . 5 |- ( x = z -> ( ph <-> [ z / x ] ph ) )
8	6, 7	anbi12d 716	. . . 4 |- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
9	1, 5, 8	cbvab 2573	. . 3 |- { x | ( x e. A /\ ph ) } = { z | ( z e. A /\ [ z / x ] ph ) }
10		cbvrab.2	. . . . . 6 |- F/_ y A
11	10	nfcri 2585	. . . . 5 |- F/ y z e. A
12		cbvrab.3	. . . . . 6 |- F/ y ph
13	12	nfsb 2268	. . . . 5 |- F/ y [ z / x ] ph
14	11, 13	nfan 2010	. . . 4 |- F/ y ( z e. A /\ [ z / x ] ph )
15		nfv 1760	. . . 4 |- F/ z ( y e. A /\ ps )
16		eleq1 2516	. . . . 5 |- ( z = y -> ( z e. A <-> y e. A ) )
17		sbequ 2204	. . . . . 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 2236	. . . . . 6 |- ( [ y / x ] ph <-> ps )
21	17, 20	syl6bb 265	. . . . 5 |- ( z = y -> ( [ z / x ] ph <-> ps ) )
22	16, 21	anbi12d 716	. . . 4 |- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
23	14, 15, 22	cbvab 2573	. . 3 |- { z | ( z e. A /\ [ z / x ] ph ) } = { y | ( y e. A /\ ps ) }
24	9, 23	eqtri 2472	. 2 |- { x | ( x e. A /\ ph ) } = { y | ( y e. A /\ ps ) }
25		df-rab 2745	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
26		df-rab 2745	. 2 |- { y e. A | ps } = { y | ( y e. A /\ ps ) }
27	24, 25, 26	3eqtr4i 2482	1 |- { x e. A | ph } = { y e. A | ps }

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   = wceq 1443   F/wnf 1666   [wsb 1796   e. wcel 1886   {cab 2436   F/_wnfc 2578   {crab 2740

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-rab 2745

This theorem is referenced by:  cbvrabv  3043  elrabsf  3305  tfis  6678  cantnflem1  8191  scottexs  8355  scott0s  8356  elmptrab  20835  suppss2fOLD  28230  bnj1534  29657  scottexf  32404  scott0f  32405  eq0rabdioph  35613  rexrabdioph  35631  rexfrabdioph  35632  elnn0rabdioph  35640  dvdsrabdioph  35647  binomcxplemdvsum  36698  stoweidlem34  37889  stoweidlem59  37914