Theorem boxcutc 7951

Description: The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.)

Assertion

Ref	Expression
boxcutc	|- ( ( X e. A /\ A. k e. A C C_ B ) -> ( X_ k e. A B \ X_ k e. A if ( k = X , C , B ) ) = X_ k e. A if ( k = X , ( B \ C ) , B ) )

Distinct variable groups:   A, k   k, X

Allowed substitution hints:   B( k)   C( k)

Proof of Theorem boxcutc

Dummy variables l m z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eldifi 3732	. . 3 |- ( z e. ( X_ k e. A B \ X_ k e. A if ( k = X , C , B ) ) -> z e. X_ k e. A B )
2	1	adantl 482	. 2 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. ( X_ k e. A B \ X_ k e. A if ( k = X , C , B ) ) ) -> z e. X_ k e. A B )
3		sseq1 3626	. . . . . 6 |- ( ( B \ C ) = if ( k = X , ( B \ C ) , B ) -> ( ( B \ C ) C_ B <-> if ( k = X , ( B \ C ) , B ) C_ B ) )
4		sseq1 3626	. . . . . 6 |- ( B = if ( k = X , ( B \ C ) , B ) -> ( B C_ B <-> if ( k = X , ( B \ C ) , B ) C_ B ) )
5		difss 3737	. . . . . 6 |- ( B \ C ) C_ B
6		ssid 3624	. . . . . 6 |- B C_ B
7	3, 4, 5, 6	keephyp 4152	. . . . 5 |- if ( k = X , ( B \ C ) , B ) C_ B
8	7	rgenw 2924	. . . 4 |- A. k e. A if ( k = X , ( B \ C ) , B ) C_ B
9		ss2ixp 7921	. . . 4 |- ( A. k e. A if ( k = X , ( B \ C ) , B ) C_ B -> X_ k e. A if ( k = X , ( B \ C ) , B ) C_ X_ k e. A B )
10	8, 9	mp1i 13	. . 3 |- ( ( X e. A /\ A. k e. A C C_ B ) -> X_ k e. A if ( k = X , ( B \ C ) , B ) C_ X_ k e. A B )
11	10	sselda 3603	. 2 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A if ( k = X , ( B \ C ) , B ) ) -> z e. X_ k e. A B )
12		ixpfn 7914	. . . . . . . . 9 |- ( z e. X_ k e. A B -> z Fn A )
13	12	adantl 482	. . . . . . . 8 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> z Fn A )
14	13	biantrurd 529	. . . . . . 7 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( A. k e. A ( z ` k ) e. if ( k = X , C , B ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = X , C , B ) ) ) )
15		vex 3203	. . . . . . . 8 |- z e. _V
16	15	elixp 7915	. . . . . . 7 |- ( z e. X_ k e. A if ( k = X , C , B ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = X , C , B ) ) )
17	14, 16	syl6rbbr 279	. . . . . 6 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( z e. X_ k e. A if ( k = X , C , B ) <-> A. k e. A ( z ` k ) e. if ( k = X , C , B ) ) )
18	17	notbid 308	. . . . 5 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( -. z e. X_ k e. A if ( k = X , C , B ) <-> -. A. k e. A ( z ` k ) e. if ( k = X , C , B ) ) )
19		rexnal 2995	. . . . . 6 |- ( E. k e. A -. ( z ` k ) e. if ( k = X , C , B ) <-> -. A. k e. A ( z ` k ) e. if ( k = X , C , B ) )
20		eleq2 2690	. . . . . . . . . 10 |- ( ( [_ m / k ]_ B \ [_ m / k ]_ C ) = if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) -> ( ( z ` m ) e. ( [_ m / k ]_ B \ [_ m / k ]_ C ) <-> ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) )
21		eleq2 2690	. . . . . . . . . 10 |- ( [_ m / k ]_ B = if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) -> ( ( z ` m ) e. [_ m / k ]_ B <-> ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) )
22		eleq2 2690	. . . . . . . . . . . . . . . . . . 19 |- ( [_ l / k ]_ C = if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) -> ( ( z ` l ) e. [_ l / k ]_ C <-> ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) )
23		eleq2 2690	. . . . . . . . . . . . . . . . . . 19 |- ( [_ l / k ]_ B = if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) -> ( ( z ` l ) e. [_ l / k ]_ B <-> ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) )
24		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( X e. A /\ A. k e. A C C_ B ) -> X e. A )
25	15	elixp 7915	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( z e. X_ k e. A B <-> ( z Fn A /\ A. k e. A ( z ` k ) e. B ) )
26	25	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z e. X_ k e. A B -> A. k e. A ( z ` k ) e. B )
27		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/ l ( z ` k ) e. B
28		nfcsb1v 3549	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- F/_ k [_ l / k ]_ B
29	28	nfel2 2781	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- F/ k ( z ` l ) e. [_ l / k ]_ B
30		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( k = l -> ( z ` k ) = ( z ` l ) )
31		csbeq1a 3542	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( k = l -> B = [_ l / k ]_ B )
32	30, 31	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( k = l -> ( ( z ` k ) e. B <-> ( z ` l ) e. [_ l / k ]_ B ) )
33	27, 29, 32	cbvral 3167	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( A. k e. A ( z ` k ) e. B <-> A. l e. A ( z ` l ) e. [_ l / k ]_ B )
34	26, 33	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( z e. X_ k e. A B -> A. l e. A ( z ` l ) e. [_ l / k ]_ B )
35		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( l = X -> ( z ` l ) = ( z ` X ) )
36		csbeq1 3536	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( l = X -> [_ l / k ]_ B = [_ X / k ]_ B )
37	35, 36	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( l = X -> ( ( z ` l ) e. [_ l / k ]_ B <-> ( z ` X ) e. [_ X / k ]_ B ) )
38	37	rspcva 3307	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( X e. A /\ A. l e. A ( z ` l ) e. [_ l / k ]_ B ) -> ( z ` X ) e. [_ X / k ]_ B )
39	24, 34, 38	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( z ` X ) e. [_ X / k ]_ B )
40		neldif 3735	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( z ` X ) e. [_ X / k ]_ B /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) -> ( z ` X ) e. [_ X / k ]_ C )
41	39, 40	sylan 488	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) -> ( z ` X ) e. [_ X / k ]_ C )
42	41	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) /\ l e. A ) -> ( z ` X ) e. [_ X / k ]_ C )
43		csbeq1 3536	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l = X -> [_ l / k ]_ C = [_ X / k ]_ C )
44	35, 43	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . 21 |- ( l = X -> ( ( z ` l ) e. [_ l / k ]_ C <-> ( z ` X ) e. [_ X / k ]_ C ) )
45	42, 44	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) /\ l e. A ) -> ( l = X -> ( z ` l ) e. [_ l / k ]_ C ) )
46	45	imp 445	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) /\ l e. A ) /\ l = X ) -> ( z ` l ) e. [_ l / k ]_ C )
47	34	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) -> A. l e. A ( z ` l ) e. [_ l / k ]_ B )
48	47	r19.21bi 2932	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) /\ l e. A ) -> ( z ` l ) e. [_ l / k ]_ B )
49	48	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) /\ l e. A ) /\ -. l = X ) -> ( z ` l ) e. [_ l / k ]_ B )
50	22, 23, 46, 49	ifbothda 4123	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) /\ l e. A ) -> ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
51	50	ralrimiva 2966	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) -> A. l e. A ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
52		dfral2 2994	. . . . . . . . . . . . . . . . 17 |- ( A. l e. A ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) <-> -. E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
53	51, 52	sylib 208	. . . . . . . . . . . . . . . 16 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) -> -. E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
54	53	ex 450	. . . . . . . . . . . . . . 15 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( -. ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) -> -. E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) )
55	54	con4d 114	. . . . . . . . . . . . . 14 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) -> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) )
56	55	imp 445	. . . . . . . . . . . . 13 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) -> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
57	56	adantr 481	. . . . . . . . . . . 12 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) /\ m e. A ) -> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
58		fveq2 6191	. . . . . . . . . . . . 13 |- ( m = X -> ( z ` m ) = ( z ` X ) )
59		csbeq1 3536	. . . . . . . . . . . . . 14 |- ( m = X -> [_ m / k ]_ B = [_ X / k ]_ B )
60		csbeq1 3536	. . . . . . . . . . . . . 14 |- ( m = X -> [_ m / k ]_ C = [_ X / k ]_ C )
61	59, 60	difeq12d 3729	. . . . . . . . . . . . 13 |- ( m = X -> ( [_ m / k ]_ B \ [_ m / k ]_ C ) = ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
62	58, 61	eleq12d 2695	. . . . . . . . . . . 12 |- ( m = X -> ( ( z ` m ) e. ( [_ m / k ]_ B \ [_ m / k ]_ C ) <-> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) )
63	57, 62	syl5ibrcom 237	. . . . . . . . . . 11 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) /\ m e. A ) -> ( m = X -> ( z ` m ) e. ( [_ m / k ]_ B \ [_ m / k ]_ C ) ) )
64	63	imp 445	. . . . . . . . . 10 |- ( ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) /\ m e. A ) /\ m = X ) -> ( z ` m ) e. ( [_ m / k ]_ B \ [_ m / k ]_ C ) )
65		nfv 1843	. . . . . . . . . . . . . . 15 |- F/ m ( z ` k ) e. B
66		nfcsb1v 3549	. . . . . . . . . . . . . . . 16 |- F/_ k [_ m / k ]_ B
67	66	nfel2 2781	. . . . . . . . . . . . . . 15 |- F/ k ( z ` m ) e. [_ m / k ]_ B
68		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( k = m -> ( z ` k ) = ( z ` m ) )
69		csbeq1a 3542	. . . . . . . . . . . . . . . 16 |- ( k = m -> B = [_ m / k ]_ B )
70	68, 69	eleq12d 2695	. . . . . . . . . . . . . . 15 |- ( k = m -> ( ( z ` k ) e. B <-> ( z ` m ) e. [_ m / k ]_ B ) )
71	65, 67, 70	cbvral 3167	. . . . . . . . . . . . . 14 |- ( A. k e. A ( z ` k ) e. B <-> A. m e. A ( z ` m ) e. [_ m / k ]_ B )
72	26, 71	sylib 208	. . . . . . . . . . . . 13 |- ( z e. X_ k e. A B -> A. m e. A ( z ` m ) e. [_ m / k ]_ B )
73	72	ad2antlr 763	. . . . . . . . . . . 12 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) -> A. m e. A ( z ` m ) e. [_ m / k ]_ B )
74	73	r19.21bi 2932	. . . . . . . . . . 11 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) /\ m e. A ) -> ( z ` m ) e. [_ m / k ]_ B )
75	74	adantr 481	. . . . . . . . . 10 |- ( ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) /\ m e. A ) /\ -. m = X ) -> ( z ` m ) e. [_ m / k ]_ B )
76	20, 21, 64, 75	ifbothda 4123	. . . . . . . . 9 |- ( ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) /\ m e. A ) -> ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) )
77	76	ralrimiva 2966	. . . . . . . 8 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) -> A. m e. A ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) )
78		simpll 790	. . . . . . . . 9 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> X e. A )
79		iftrue 4092	. . . . . . . . . . . . . 14 |- ( m = X -> if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) = ( [_ m / k ]_ B \ [_ m / k ]_ C ) )
80	79, 61	eqtrd 2656	. . . . . . . . . . . . 13 |- ( m = X -> if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) = ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
81	58, 80	eleq12d 2695	. . . . . . . . . . . 12 |- ( m = X -> ( ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) <-> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) )
82	81	rspcva 3307	. . . . . . . . . . 11 |- ( ( X e. A /\ A. m e. A ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) -> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
83	78, 82	sylan 488	. . . . . . . . . 10 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ A. m e. A ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) -> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
84	83	eldifbd 3587	. . . . . . . . 9 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ A. m e. A ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) -> -. ( z ` X ) e. [_ X / k ]_ C )
85		iftrue 4092	. . . . . . . . . . . . 13 |- ( l = X -> if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) = [_ l / k ]_ C )
86	85, 43	eqtrd 2656	. . . . . . . . . . . 12 |- ( l = X -> if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) = [_ X / k ]_ C )
87	35, 86	eleq12d 2695	. . . . . . . . . . 11 |- ( l = X -> ( ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) <-> ( z ` X ) e. [_ X / k ]_ C ) )
88	87	notbid 308	. . . . . . . . . 10 |- ( l = X -> ( -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) <-> -. ( z ` X ) e. [_ X / k ]_ C ) )
89	88	rspcev 3309	. . . . . . . . 9 |- ( ( X e. A /\ -. ( z ` X ) e. [_ X / k ]_ C ) -> E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
90	78, 84, 89	syl2an2r 876	. . . . . . . 8 |- ( ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) /\ A. m e. A ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) -> E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
91	77, 90	impbida 877	. . . . . . 7 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) <-> A. m e. A ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) )
92		nfv 1843	. . . . . . . 8 |- F/ l -. ( z ` k ) e. if ( k = X , C , B )
93		nfv 1843	. . . . . . . . . . 11 |- F/ k l = X
94		nfcsb1v 3549	. . . . . . . . . . 11 |- F/_ k [_ l / k ]_ C
95	93, 94, 28	nfif 4115	. . . . . . . . . 10 |- F/_ k if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B )
96	95	nfel2 2781	. . . . . . . . 9 |- F/ k ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B )
97	96	nfn 1784	. . . . . . . 8 |- F/ k -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B )
98		eqeq1 2626	. . . . . . . . . . 11 |- ( k = l -> ( k = X <-> l = X ) )
99		csbeq1a 3542	. . . . . . . . . . 11 |- ( k = l -> C = [_ l / k ]_ C )
100	98, 99, 31	ifbieq12d 4113	. . . . . . . . . 10 |- ( k = l -> if ( k = X , C , B ) = if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
101	30, 100	eleq12d 2695	. . . . . . . . 9 |- ( k = l -> ( ( z ` k ) e. if ( k = X , C , B ) <-> ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) )
102	101	notbid 308	. . . . . . . 8 |- ( k = l -> ( -. ( z ` k ) e. if ( k = X , C , B ) <-> -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) ) )
103	92, 97, 102	cbvrex 3168	. . . . . . 7 |- ( E. k e. A -. ( z ` k ) e. if ( k = X , C , B ) <-> E. l e. A -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
104		nfv 1843	. . . . . . . 8 |- F/ m ( z ` k ) e. if ( k = X , ( B \ C ) , B )
105		nfv 1843	. . . . . . . . . 10 |- F/ k m = X
106		nfcsb1v 3549	. . . . . . . . . . 11 |- F/_ k [_ m / k ]_ C
107	66, 106	nfdif 3731	. . . . . . . . . 10 |- F/_ k ( [_ m / k ]_ B \ [_ m / k ]_ C )
108	105, 107, 66	nfif 4115	. . . . . . . . 9 |- F/_ k if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B )
109	108	nfel2 2781	. . . . . . . 8 |- F/ k ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B )
110		eqeq1 2626	. . . . . . . . . 10 |- ( k = m -> ( k = X <-> m = X ) )
111		csbeq1a 3542	. . . . . . . . . . 11 |- ( k = m -> C = [_ m / k ]_ C )
112	69, 111	difeq12d 3729	. . . . . . . . . 10 |- ( k = m -> ( B \ C ) = ( [_ m / k ]_ B \ [_ m / k ]_ C ) )
113	110, 112, 69	ifbieq12d 4113	. . . . . . . . 9 |- ( k = m -> if ( k = X , ( B \ C ) , B ) = if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) )
114	68, 113	eleq12d 2695	. . . . . . . 8 |- ( k = m -> ( ( z ` k ) e. if ( k = X , ( B \ C ) , B ) <-> ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) ) )
115	104, 109, 114	cbvral 3167	. . . . . . 7 |- ( A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) <-> A. m e. A ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) )
116	91, 103, 115	3bitr4g 303	. . . . . 6 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( E. k e. A -. ( z ` k ) e. if ( k = X , C , B ) <-> A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) ) )
117	19, 116	syl5bbr 274	. . . . 5 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( -. A. k e. A ( z ` k ) e. if ( k = X , C , B ) <-> A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) ) )
118	18, 117	bitrd 268	. . . 4 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( -. z e. X_ k e. A if ( k = X , C , B ) <-> A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) ) )
119		ibar 525	. . . . 5 |- ( z e. X_ k e. A B -> ( -. z e. X_ k e. A if ( k = X , C , B ) <-> ( z e. X_ k e. A B /\ -. z e. X_ k e. A if ( k = X , C , B ) ) ) )
120	119	adantl 482	. . . 4 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( -. z e. X_ k e. A if ( k = X , C , B ) <-> ( z e. X_ k e. A B /\ -. z e. X_ k e. A if ( k = X , C , B ) ) ) )
121	13	biantrurd 529	. . . 4 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) ) ) )
122	118, 120, 121	3bitr3d 298	. . 3 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( ( z e. X_ k e. A B /\ -. z e. X_ k e. A if ( k = X , C , B ) ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) ) ) )
123		eldif 3584	. . 3 |- ( z e. ( X_ k e. A B \ X_ k e. A if ( k = X , C , B ) ) <-> ( z e. X_ k e. A B /\ -. z e. X_ k e. A if ( k = X , C , B ) ) )
124	15	elixp 7915	. . 3 |- ( z e. X_ k e. A if ( k = X , ( B \ C ) , B ) <-> ( z Fn A /\ A. k e. A ( z ` k ) e. if ( k = X , ( B \ C ) , B ) ) )
125	122, 123, 124	3bitr4g 303	. 2 |- ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> ( z e. ( X_ k e. A B \ X_ k e. A if ( k = X , C , B ) ) <-> z e. X_ k e. A if ( k = X , ( B \ C ) , B ) ) )
126	2, 11, 125	eqrdav 2621	1 |- ( ( X e. A /\ A. k e. A C C_ B ) -> ( X_ k e. A B \ X_ k e. A if ( k = X , C , B ) ) = X_ k e. A if ( k = X , ( B \ C ) , B ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   E.wrex 2913   [_csb 3533   \ cdif 3571   C_ wss 3574   ifcif 4086   Fn wfn 5883   ` cfv 5888   X_cixp 7908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-ixp 7909

This theorem is referenced by:  ptcld  21416