Theorem cbvrab 3093

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 1694	. . . 4 |- F/ z ( x e. A /\ ph )
2		cbvrab.1	. . . . . 6 |- F/_ x A
3	2	nfcri 2598	. . . . 5 |- F/ x z e. A
4		nfs1v 2167	. . . . 5 |- F/ x [ z / x ] ph
5	3, 4	nfan 1914	. . . 4 |- F/ x ( z e. A /\ [ z / x ] ph )
6		eleq1 2515	. . . . 5 |- ( x = z -> ( x e. A <-> z e. A ) )
7		sbequ12 1978	. . . . 5 |- ( x = z -> ( ph <-> [ z / x ] ph ) )
8	6, 7	anbi12d 710	. . . 4 |- ( x = z -> ( ( x e. A /\ ph ) <-> ( z e. A /\ [ z / x ] ph ) ) )
9	1, 5, 8	cbvab 2584	. . 3 |- { x | ( x e. A /\ ph ) } = { z | ( z e. A /\ [ z / x ] ph ) }
10		cbvrab.2	. . . . . 6 |- F/_ y A
11	10	nfcri 2598	. . . . 5 |- F/ y z e. A
12		cbvrab.3	. . . . . 6 |- F/ y ph
13	12	nfsb 2170	. . . . 5 |- F/ y [ z / x ] ph
14	11, 13	nfan 1914	. . . 4 |- F/ y ( z e. A /\ [ z / x ] ph )
15		nfv 1694	. . . 4 |- F/ z ( y e. A /\ ps )
16		eleq1 2515	. . . . 5 |- ( z = y -> ( z e. A <-> y e. A ) )
17		sbequ 2103	. . . . . 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 2135	. . . . . 6 |- ( [ y / x ] ph <-> ps )
21	17, 20	syl6bb 261	. . . . 5 |- ( z = y -> ( [ z / x ] ph <-> ps ) )
22	16, 21	anbi12d 710	. . . 4 |- ( z = y -> ( ( z e. A /\ [ z / x ] ph ) <-> ( y e. A /\ ps ) ) )
23	14, 15, 22	cbvab 2584	. . 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 2802	. 2 |- { x e. A | ph } = { x | ( x e. A /\ ph ) }
26		df-rab 2802	. 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 184   /\ wa 369   = wceq 1383   F/wnf 1603   [wsb 1726   e. wcel 1804   {cab 2428   F/_wnfc 2591   {crab 2797

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-rab 2802

This theorem is referenced by:  cbvrabv  3094  elrabsf  3352  tfis  6674  cantnflem1  8111  scottexs  8308  scott0s  8309  elmptrab  20201  suppss2f  27349  scottexf  30551  scott0f  30552  eq0rabdioph  30685  rexrabdioph  30702  rexfrabdioph  30703  elnn0rabdioph  30711  dvdsrabdioph  30718  stoweidlem34  31705  stoweidlem59  31730  bnj1534  33644