Theorem cbvrab 2968

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 1678	. . . 4 |- F/ z ( x e. A /\ ph )
2		cbvrab.1	. . . . . 6 |- F/_ x A
3	2	nfcri 2571	. . . . 5 |- F/ x z e. A
4		nfs1v 2147	. . . . 5 |- F/ x [ z / x ] ph
5	3, 4	nfan 1865	. . . 4 |- F/ x ( z e. A /\ [ z / x ] ph )
6		eleq1 2501	. . . . 5 |- ( x = z -> ( x e. A <-> z e. A ) )
7		sbequ12 1941	. . . . 5 |- ( x = z -> ( ph <-> [ z / x ] ph ) )
8	6, 7	anbi12d 705	. . . 4 |- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
9	1, 5, 8	cbvab 2559	. . 3 |- { x | ( x e. A /\ ph ) } = { z | ( z e. A /\ [ z / x ] ph ) }
10		cbvrab.2	. . . . . 6 |- F/_ y A
11	10	nfcri 2571	. . . . 5 |- F/ y z e. A
12		cbvrab.3	. . . . . 6 |- F/ y ph
13	12	nfsb 2151	. . . . 5 |- F/ y [ z / x ] ph
14	11, 13	nfan 1865	. . . 4 |- F/ y ( z e. A /\ [ z / x ] ph )
15		nfv 1678	. . . 4 |- F/ z ( y e. A /\ ps )
16		eleq1 2501	. . . . 5 |- ( z = y -> ( z e. A <-> y e. A ) )
17		sbequ 2072	. . . . . 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 2105	. . . . . 6 |- ( [ y / x ] ph <-> ps )
21	17, 20	syl6bb 261	. . . . 5 |- ( z = y -> ( [ z / x ] ph <-> ps ) )
22	16, 21	anbi12d 705	. . . 4 |- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
23	14, 15, 22	cbvab 2559	. . 3 |- { z | ( z e. A /\ [ z / x ] ph ) } = { y | ( y e. A /\ ps ) }
24	9, 23	eqtri 2461	. 2 |- { x | ( x e. A /\ ph ) } = { y | ( y e. A /\ ps ) }
25		df-rab 2722	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
26		df-rab 2722	. 2 |- { y e. A | ps } = { y | ( y e. A /\ ps ) }
27	24, 25, 26	3eqtr4i 2471	1 |- { x e. A | ph } = { y e. A | ps }

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1364   F/wnf 1594   [wsb 1705   e. wcel 1761   {cab 2427   F/_wnfc 2564   {crab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722

This theorem is referenced by:  cbvrabv  2969  elrabsf  3222  tfis  6464  cantnflem1  7893  scottexs  8090  scott0s  8091  elmptrab  19359  suppss2f  25889  scottexf  28905  scott0f  28906  eq0rabdioph  29040  rexrabdioph  29057  rexfrabdioph  29058  elnn0rabdioph  29066  dvdsrabdioph  29073  stoweidlem34  29754  stoweidlem59  29779  bnj1534  31680