Theorem cbvralcsf 16411

Description: A more general version of cbvralf 2276 that doesn't require A and B to be distinct from x or y. Changes bound variables using implicit substitution.

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
cbvralcsf	|- (A.x e. A ph <-> A.y e. B ps)

Distinct variable groups:   w,A   w,B

Proof of Theorem cbvralcsf

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	hbim 1354	. . . 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	imbi12d 688	. . . 4 |- (x = z -> ((x e. A -> ph) <-> (z e. [_z / x]_A -> [z / x]ph)))
13	1, 7, 12	cbval 1527	. . 3 |- (A.x(x e. A -> ph) <-> A.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	hbim 1354	. . . 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	imbi12d 688	. . . 4 |- (z = y -> ((z e. [_z / x]_A -> [z / x]ph) <-> (y e. B -> ps)))
43	22, 23, 42	cbval 1527	. . 3 |- (A.z(z e. [_z / x]_A -> [z / x]ph) <-> A.y(y e. B -> ps))
44	13, 43	bitri 190	. 2 |- (A.x(x e. A -> ph) <-> A.y(y e. B -> ps))
45		df-ral 2109	. 2 |- (A.x e. A ph <-> A.x(x e. A -> ph))
46		df-ral 2109	. 2 |- (A.y e. B ps <-> A.y(y e. B -> ps))
47	44, 45, 46	3bitr4i 200	1 |- (A.x e. A ph <-> A.y e. B ps)

Syntax hints:   -> wi 3   <-> wb 163  A.wal 1296   = wceq 1298   e. wcel 1300  [wsbc 1534  {cab 1871  A.wral 2105  _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-ral 2109  df-v 2294  df-sbc 2454  df-csb 2541

Copyright terms: Public domain