Theorem cbvrabcsf 16414

Description: A more general version of cbvrab 2421 with no distinct variable restrictions.

Hypotheses

Ref	Expression
cbvralcsf.1	|- (x = y -> A = B)
cbvralcsf.2	|- (x = y -> (ph <-> ps))
cbvralcsf.3	|- (w e. A -> A.y w e. A)
cbvralcsf.4	|- (w e. B -> A.x w e. B)
cbvralcsf.5	|- (ph -> A.yph)
cbvralcsf.6	|- (ps -> A.xps)

Assertion

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

Distinct variable groups:   w,A   w,B

Proof of Theorem cbvrabcsf

Step	Hyp	Ref	Expression
1		ax-17 1317	. . . 4 |- ((x e. A /\ ph) -> A.z(x e. A /\ ph))
2		ax-17 1317	. . . . . 6 |- (v e. z -> A.x v e. z)
3		visset 2295	. . . . . . 7 |- z e. _V
4	3, 2	hbcsb1 2568	. . . . . 6 |- (v e. [_z / x]_A -> A.x v e. [_z / x]_A)
5	2, 4	hbel 1996	. . . . 5 |- (z e. [_z / x]_A -> A.x z e. [_z / x]_A)
6		hbs1 1722	. . . . 5 |- ([z / x]ph -> A.x[z / x]ph)
7	5, 6	hban 1356	. . . 4 |- ((z e. [_z / x]_A /\ [z / x]ph) -> A.x(z e. [_z / x]_A /\ [z / x]ph))
8		id 73	. . . . . 6 |- (x = z -> x = z)
9		csbeq1a 2546	. . . . . 6 |- (x = z -> A = [_z / x]_A)
10	8, 9	eleq12d 1965	. . . . 5 |- (x = z -> (x e. A <-> z e. [_z / x]_A))
11		sbequ12 1545	. . . . 5 |- (x = z -> (ph <-> [z / x]ph))
12	10, 11	anbi12d 690	. . . 4 |- (x = z -> ((x e. A /\ ph) <-> (z e. [_z / x]_A /\ [z / x]ph)))
13	1, 7, 12	cbvab 2419	. . 3 |- {x | (x e. A /\ ph)} = {z | (z e. [_z / x]_A /\ [z / x]ph)}
14		ax-17 1317	. . . . . 6 |- (v e. z -> A.y v e. z)
15		cbvralcsf.3	. . . . . . . . 9 |- (w e. A -> A.y w e. A)
16	15	hblem 1993	. . . . . . . 8 |- (v e. A -> A.y v e. A)
17	14, 16	hbcsbg 2569	. . . . . . 7 |- (z e. _V -> (v e. [_z / x]_A -> A.y v e. [_z / x]_A))
18	3, 17	ax-mp 7	. . . . . 6 |- (v e. [_z / x]_A -> A.y v e. [_z / x]_A)
19	14, 18	hbel 1996	. . . . 5 |- (z e. [_z / x]_A -> A.y z e. [_z / x]_A)
20		cbvralcsf.5	. . . . . 6 |- (ph -> A.yph)
21	20	hbsb 1723	. . . . 5 |- ([z / x]ph -> A.y[z / x]ph)
22	19, 21	hban 1356	. . . 4 |- ((z e. [_z / x]_A /\ [z / x]ph) -> A.y(z e. [_z / x]_A /\ [z / x]ph))
23		ax-17 1317	. . . 4 |- ((y e. B /\ ps) -> A.z(y e. B /\ ps))
24		id 73	. . . . . 6 |- (z = y -> z = y)
25		csbeq1 2542	. . . . . . 7 |- (z = y -> [_z / x]_A = [_y / x]_A)
26		df-csb 2541	. . . . . . . 8 |- [_y / x]_A = {v | [y / x]v e. A}
27		cbvralcsf.4	. . . . . . . . . . . 12 |- (w e. B -> A.x w e. B)
28	27	hblem 1993	. . . . . . . . . . 11 |- (v e. B -> A.x v e. B)
29		cbvralcsf.1	. . . . . . . . . . . 12 |- (x = y -> A = B)
30	29	eleq2d 1964	. . . . . . . . . . 11 |- (x = y -> (v e. A <-> v e. B))
31	28, 30	sbie 1565	. . . . . . . . . 10 |- ([y / x]v e. A <-> v e. B)
32	31	bicomi 189	. . . . . . . . 9 |- (v e. B <-> [y / x]v e. A)
33	32	abbi2i 2005	. . . . . . . 8 |- B = {v | [y / x]v e. A}
34	26, 33	eqtr4i 1911	. . . . . . 7 |- [_y / x]_A = B
35	25, 34	syl6eq 1944	. . . . . 6 |- (z = y -> [_z / x]_A = B)
36	24, 35	eleq12d 1965	. . . . 5 |- (z = y -> (z e. [_z / x]_A <-> y e. B))
37		sbequ 1599	. . . . . 6 |- (z = y -> ([z / x]ph <-> [y / x]ph))
38		cbvralcsf.6	. . . . . . 7 |- (ps -> A.xps)
39		cbvralcsf.2	. . . . . . 7 |- (x = y -> (ph <-> ps))
40	38, 39	sbie 1565	. . . . . 6 |- ([y / x]ph <-> ps)
41	37, 40	syl6bb 595	. . . . 5 |- (z = y -> ([z / x]ph <-> ps))
42	36, 41	anbi12d 690	. . . 4 |- (z = y -> ((z e. [_z / x]_A /\ [z / x]ph) <-> (y e. B /\ ps)))
43	22, 23, 42	cbvab 2419	. . 3 |- {z | (z e. [_z / x]_A /\ [z / x]ph)} = {y | (y e. B /\ ps)}
44	13, 43	eqtri 1908	. 2 |- {x | (x e. A /\ ph)} = {y | (y e. B /\ ps)}
45		df-rab 2112	. 2 |- {x e. A | ph} = {x | (x e. A /\ ph)}
46		df-rab 2112	. 2 |- {y e. B | ps} = {y | (y e. B /\ ps)}
47	44, 45, 46	3eqtr4i 1921	1 |- {x e. A | ph} = {y e. B | ps}

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  [wsbc 1534  {cab 1871  {crab 2108  _Vcvv 2292  [_csb 2540

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  df-v 2294  df-sbc 2454  df-csb 2541

Copyright terms: Public domain