This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem boxcutc

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

Ref Expression
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( B \ C ) = if ( k = X , ( B \ C ) , B ) -> ( ( B \ C ) C_ B <-> if ( k = X , ( B \ C ) , B ) C_ B ) )
4 sseq1 
 |-  ( B = if ( k = X , ( B \ C ) , B ) -> ( B C_ B <-> if ( k = X , ( B \ C ) , B ) C_ B ) )
5 difss 
 |-  ( B \ C ) C_ B
6 ssid 
 |-  B C_ B
7 3 4 5 6 keephyp 
 |-  if ( k = X , ( B \ C ) , B ) C_ B
8 7 rgenw 
 |-  A. k e. A if ( k = X , ( B \ C ) , B ) C_ B
9 ss2ixp 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( ( 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 vex 
 |-  z e. _V
13 12 elixp 
 |-  ( 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 ) ) )
14 ixpfn 
 |-  ( z e. X_ k e. A B -> z Fn A )
15 14 adantl 
 |-  ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> z Fn A )
16 15 biantrurd 
 |-  ( ( ( 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 ) ) ) )
17 13 16 bitr4id 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( ( [_ 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 
 |-  ( [_ 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 
 |-  ( [_ 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 
 |-  ( [_ 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 
 |-  ( ( X e. A /\ A. k e. A C C_ B ) -> X e. A )
25 12 elixp 
 |-  ( z e. X_ k e. A B <-> ( z Fn A /\ A. k e. A ( z ` k ) e. B ) )
26 25 simprbi 
 |-  ( z e. X_ k e. A B -> A. k e. A ( z ` k ) e. B )
27 nfv 
 |-  F/ l ( z ` k ) e. B
28 nfcsb1v 
 |-  F/_ k [_ l / k ]_ B
29 28 nfel2 
 |-  F/ k ( z ` l ) e. [_ l / k ]_ B
30 fveq2 
 |-  ( k = l -> ( z ` k ) = ( z ` l ) )
31 csbeq1a 
 |-  ( k = l -> B = [_ l / k ]_ B )
32 30 31 eleq12d 
 |-  ( k = l -> ( ( z ` k ) e. B <-> ( z ` l ) e. [_ l / k ]_ B ) )
33 27 29 32 cbvralw 
 |-  ( A. k e. A ( z ` k ) e. B <-> A. l e. A ( z ` l ) e. [_ l / k ]_ B )
34 26 33 sylib 
 |-  ( z e. X_ k e. A B -> A. l e. A ( z ` l ) e. [_ l / k ]_ B )
35 fveq2 
 |-  ( l = X -> ( z ` l ) = ( z ` X ) )
36 csbeq1 
 |-  ( l = X -> [_ l / k ]_ B = [_ X / k ]_ B )
37 35 36 eleq12d 
 |-  ( l = X -> ( ( z ` l ) e. [_ l / k ]_ B <-> ( z ` X ) e. [_ X / k ]_ B ) )
38 37 rspcva 
 |-  ( ( X e. A /\ A. l e. A ( z ` l ) e. [_ l / k ]_ B ) -> ( z ` X ) e. [_ X / k ]_ B )
39 24 34 38 syl2an 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( l = X -> [_ l / k ]_ C = [_ X / k ]_ C )
44 35 43 eleq12d 
 |-  ( l = X -> ( ( z ` l ) e. [_ l / k ]_ C <-> ( z ` X ) e. [_ X / k ]_ C ) )
45 42 44 syl5ibrcom 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( m = X -> ( z ` m ) = ( z ` X ) )
59 csbeq1 
 |-  ( m = X -> [_ m / k ]_ B = [_ X / k ]_ B )
60 csbeq1 
 |-  ( m = X -> [_ m / k ]_ C = [_ X / k ]_ C )
61 59 60 difeq12d 
 |-  ( m = X -> ( [_ m / k ]_ B \ [_ m / k ]_ C ) = ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
62 58 61 eleq12d 
 |-  ( m = X -> ( ( z ` m ) e. ( [_ m / k ]_ B \ [_ m / k ]_ C ) <-> ( z ` X ) e. ( [_ X / k ]_ B \ [_ X / k ]_ C ) ) )
63 57 62 syl5ibrcom 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  F/ m ( z ` k ) e. B
66 nfcsb1v 
 |-  F/_ k [_ m / k ]_ B
67 66 nfel2 
 |-  F/ k ( z ` m ) e. [_ m / k ]_ B
68 fveq2 
 |-  ( k = m -> ( z ` k ) = ( z ` m ) )
69 csbeq1a 
 |-  ( k = m -> B = [_ m / k ]_ B )
70 68 69 eleq12d 
 |-  ( k = m -> ( ( z ` k ) e. B <-> ( z ` m ) e. [_ m / k ]_ B ) )
71 65 67 70 cbvralw 
 |-  ( A. k e. A ( z ` k ) e. B <-> A. m e. A ( z ` m ) e. [_ m / k ]_ B )
72 26 71 sylib 
 |-  ( z e. X_ k e. A B -> A. m e. A ( z ` m ) e. [_ m / k ]_ B )
73 72 ad2antlr 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( ( ( 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 
 |-  ( ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( X e. A /\ A. k e. A C C_ B ) /\ z e. X_ k e. A B ) -> X e. A )
79 iftrue 
 |-  ( m = X -> if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) = ( [_ m / k ]_ B \ [_ m / k ]_ C ) )
80 79 61 eqtrd 
 |-  ( m = X -> if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) = ( [_ X / k ]_ B \ [_ X / k ]_ C ) )
81 58 80 eleq12d 
 |-  ( 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 
 |-  ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( l = X -> if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) = [_ l / k ]_ C )
86 85 43 eqtrd 
 |-  ( l = X -> if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) = [_ X / k ]_ C )
87 35 86 eleq12d 
 |-  ( l = X -> ( ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) <-> ( z ` X ) e. [_ X / k ]_ C ) )
88 87 notbid 
 |-  ( l = X -> ( -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) <-> -. ( z ` X ) e. [_ X / k ]_ C ) )
89 88 rspcev 
 |-  ( ( 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 
 |-  ( ( ( ( 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 
 |-  ( ( ( 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 
 |-  F/ l -. ( z ` k ) e. if ( k = X , C , B )
93 nfv 
 |-  F/ k l = X
94 nfcsb1v 
 |-  F/_ k [_ l / k ]_ C
95 93 94 28 nfif 
 |-  F/_ k if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B )
96 95 nfel2 
 |-  F/ k ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B )
97 96 nfn 
 |-  F/ k -. ( z ` l ) e. if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B )
98 eqeq1 
 |-  ( k = l -> ( k = X <-> l = X ) )
99 csbeq1a 
 |-  ( k = l -> C = [_ l / k ]_ C )
100 98 99 31 ifbieq12d 
 |-  ( k = l -> if ( k = X , C , B ) = if ( l = X , [_ l / k ]_ C , [_ l / k ]_ B ) )
101 30 100 eleq12d 
 |-  ( 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 
 |-  ( 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 cbvrexw 
 |-  ( 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 
 |-  F/ m ( z ` k ) e. if ( k = X , ( B \ C ) , B )
105 nfv 
 |-  F/ k m = X
106 nfcsb1v 
 |-  F/_ k [_ m / k ]_ C
107 66 106 nfdif 
 |-  F/_ k ( [_ m / k ]_ B \ [_ m / k ]_ C )
108 105 107 66 nfif 
 |-  F/_ k if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B )
109 108 nfel2 
 |-  F/ k ( z ` m ) e. if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B )
110 eqeq1 
 |-  ( k = m -> ( k = X <-> m = X ) )
111 csbeq1a 
 |-  ( k = m -> C = [_ m / k ]_ C )
112 69 111 difeq12d 
 |-  ( k = m -> ( B \ C ) = ( [_ m / k ]_ B \ [_ m / k ]_ C ) )
113 110 112 69 ifbieq12d 
 |-  ( k = m -> if ( k = X , ( B \ C ) , B ) = if ( m = X , ( [_ m / k ]_ B \ [_ m / k ]_ C ) , [_ m / k ]_ B ) )
114 68 113 eleq12d 
 |-  ( 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 cbvralw 
 |-  ( 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 
 |-  ( ( ( 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 bitr3id 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( 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 
 |-  ( ( ( 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 15 biantrurd 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( 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 12 elixp 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( 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 ) )