Theorem subtr 15352

Description: Transitivity of implicit substitution.

Hypotheses

Ref	Expression
subtr.1	|- (y e. A -> A.x y e. A)
subtr.2	|- (y e. B -> A.x y e. B)
subtr.3	|- (y e. Y -> A.x y e. Y)
subtr.4	|- (y e. Z -> A.x y e. Z)
subtr.5	|- (x = A -> X = Y)
subtr.6	|- (x = B -> X = Z)

Assertion

Ref	Expression
subtr	|- ((A e. C /\ B e. D) -> (A = B -> Y = Z))

Distinct variable groups:   y,A   y,B   y,X   y,Y   y,Z   x,y

Proof of Theorem subtr

Step	Hyp	Ref	Expression
1		eqeq1 1890	. . 3 |- (z = A -> (z = w <-> A = w))
2		a9e 1483	. . . . 5 |- E.x x = z
3		ax-17 1317	. . . . . . . 8 |- (y e. z -> A.x y e. z)
4		subtr.1	. . . . . . . 8 |- (y e. A -> A.x y e. A)
5	3, 4	hbeq 1995	. . . . . . 7 |- (z = A -> A.x z = A)
6		visset 2295	. . . . . . . . 9 |- z e. _V
7	6, 3	hbcsb1 2568	. . . . . . . 8 |- (y e. [_z / x]_X -> A.x y e. [_z / x]_X)
8		subtr.3	. . . . . . . 8 |- (y e. Y -> A.x y e. Y)
9	7, 8	hbeq 1995	. . . . . . 7 |- ([_z / x]_X = Y -> A.x[_z / x]_X = Y)
10	5, 9	hbim 1354	. . . . . 6 |- ((z = A -> [_z / x]_X = Y) -> A.x(z = A -> [_z / x]_X = Y))
11		eqeq1 1890	. . . . . . 7 |- (x = z -> (x = A <-> z = A))
12		csbeq1a 2546	. . . . . . . . 9 |- (x = z -> X = [_z / x]_X)
13		subtr.5	. . . . . . . . 9 |- (x = A -> X = Y)
14	12, 13	sylan9req 1950	. . . . . . . 8 |- ((x = z /\ x = A) -> [_z / x]_X = Y)
15	14	ex 402	. . . . . . 7 |- (x = z -> (x = A -> [_z / x]_X = Y))
16	11, 15	sylbird 222	. . . . . 6 |- (x = z -> (z = A -> [_z / x]_X = Y))
17	10, 16	19.23ai 1412	. . . . 5 |- (E.x x = z -> (z = A -> [_z / x]_X = Y))
18	2, 17	ax-mp 7	. . . 4 |- (z = A -> [_z / x]_X = Y)
19	18	eqeq1d 1892	. . 3 |- (z = A -> ([_z / x]_X = [_w / x]_X <-> Y = [_w / x]_X))
20	1, 19	imbi12d 688	. 2 |- (z = A -> ((z = w -> [_z / x]_X = [_w / x]_X) <-> (A = w -> Y = [_w / x]_X)))
21		eqeq2 1893	. . 3 |- (w = B -> (A = w <-> A = B))
22		a9e 1483	. . . . 5 |- E.x x = w
23		ax-17 1317	. . . . . . . 8 |- (y e. w -> A.x y e. w)
24		subtr.2	. . . . . . . 8 |- (y e. B -> A.x y e. B)
25	23, 24	hbeq 1995	. . . . . . 7 |- (w = B -> A.x w = B)
26		visset 2295	. . . . . . . . 9 |- w e. _V
27	26, 23	hbcsb1 2568	. . . . . . . 8 |- (y e. [_w / x]_X -> A.x y e. [_w / x]_X)
28		subtr.4	. . . . . . . 8 |- (y e. Z -> A.x y e. Z)
29	27, 28	hbeq 1995	. . . . . . 7 |- ([_w / x]_X = Z -> A.x[_w / x]_X = Z)
30	25, 29	hbim 1354	. . . . . 6 |- ((w = B -> [_w / x]_X = Z) -> A.x(w = B -> [_w / x]_X = Z))
31		eqeq1 1890	. . . . . . 7 |- (x = w -> (x = B <-> w = B))
32		csbeq1a 2546	. . . . . . . . 9 |- (x = w -> X = [_w / x]_X)
33		subtr.6	. . . . . . . . 9 |- (x = B -> X = Z)
34	32, 33	sylan9req 1950	. . . . . . . 8 |- ((x = w /\ x = B) -> [_w / x]_X = Z)
35	34	ex 402	. . . . . . 7 |- (x = w -> (x = B -> [_w / x]_X = Z))
36	31, 35	sylbird 222	. . . . . 6 |- (x = w -> (w = B -> [_w / x]_X = Z))
37	30, 36	19.23ai 1412	. . . . 5 |- (E.x x = w -> (w = B -> [_w / x]_X = Z))
38	22, 37	ax-mp 7	. . . 4 |- (w = B -> [_w / x]_X = Z)
39	38	eqeq2d 1895	. . 3 |- (w = B -> (Y = [_w / x]_X <-> Y = Z))
40	21, 39	imbi12d 688	. 2 |- (w = B -> ((A = w -> Y = [_w / x]_X) <-> (A = B -> Y = Z)))
41		csbeq1 2542	. 2 |- (z = w -> [_z / x]_X = [_w / x]_X)
42	20, 40, 41	vtocl2g 2349	1 |- ((A e. C /\ B e. D) -> (A = B -> Y = Z))

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  [_csb 2540

This theorem is referenced by:  cbvcsb 15354

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

Copyright terms: Public domain