MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  boxcutc Unicode version

Theorem boxcutc 7532
Description: The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015.)
Assertion
Ref Expression
boxcutc
Distinct variable groups:   ,   ,

Proof of Theorem boxcutc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eldifi 3625 . . 3
21adantl 466 . 2
3 sseq1 3524 . . . . . 6
4 sseq1 3524 . . . . . 6
5 difss 3630 . . . . . 6
6 ssid 3522 . . . . . 6
73, 4, 5, 6keephyp 4006 . . . . 5
87rgenw 2818 . . . 4
9 ss2ixp 7502 . . . 4
108, 9mp1i 12 . . 3
1110sselda 3503 . 2
12 ixpfn 7495 . . . . . . . . 9
1312adantl 466 . . . . . . . 8
1413biantrurd 508 . . . . . . 7
15 vex 3112 . . . . . . . 8
1615elixp 7496 . . . . . . 7
1714, 16syl6rbbr 264 . . . . . 6
1817notbid 294 . . . . 5
19 rexnal 2905 . . . . . 6
20 eleq2 2530 . . . . . . . . . 10
21 eleq2 2530 . . . . . . . . . 10
22 eleq2 2530 . . . . . . . . . . . . . . . . . . 19
23 eleq2 2530 . . . . . . . . . . . . . . . . . . 19
24 simpl 457 . . . . . . . . . . . . . . . . . . . . . . . 24
2515elixp 7496 . . . . . . . . . . . . . . . . . . . . . . . . . 26
2625simprbi 464 . . . . . . . . . . . . . . . . . . . . . . . . 25
27 nfv 1707 . . . . . . . . . . . . . . . . . . . . . . . . . 26
28 nfcsb1v 3450 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
2928nfel2 2637 . . . . . . . . . . . . . . . . . . . . . . . . . 26
30 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
31 csbeq1a 3443 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
3230, 31eleq12d 2539 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3327, 29, 32cbvral 3080 . . . . . . . . . . . . . . . . . . . . . . . . 25
3426, 33sylib 196 . . . . . . . . . . . . . . . . . . . . . . . 24
35 fveq2 5871 . . . . . . . . . . . . . . . . . . . . . . . . . 26
36 csbeq1 3437 . . . . . . . . . . . . . . . . . . . . . . . . . 26
3735, 36eleq12d 2539 . . . . . . . . . . . . . . . . . . . . . . . . 25
3837rspcva 3208 . . . . . . . . . . . . . . . . . . . . . . . 24
3924, 34, 38syl2an 477 . . . . . . . . . . . . . . . . . . . . . . 23
40 neldif 3628 . . . . . . . . . . . . . . . . . . . . . . 23
4139, 40sylan 471 . . . . . . . . . . . . . . . . . . . . . 22
4241adantr 465 . . . . . . . . . . . . . . . . . . . . 21
43 csbeq1 3437 . . . . . . . . . . . . . . . . . . . . . 22
4435, 43eleq12d 2539 . . . . . . . . . . . . . . . . . . . . 21
4542, 44syl5ibrcom 222 . . . . . . . . . . . . . . . . . . . 20
4645imp 429 . . . . . . . . . . . . . . . . . . 19
4734ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21
4847r19.21bi 2826 . . . . . . . . . . . . . . . . . . . 20
4948adantr 465 . . . . . . . . . . . . . . . . . . 19
5022, 23, 46, 49ifbothda 3976 . . . . . . . . . . . . . . . . . 18
5150ralrimiva 2871 . . . . . . . . . . . . . . . . 17
52 dfral2 2904 . . . . . . . . . . . . . . . . 17
5351, 52sylib 196 . . . . . . . . . . . . . . . 16
5453ex 434 . . . . . . . . . . . . . . 15
5554con4d 105 . . . . . . . . . . . . . 14
5655imp 429 . . . . . . . . . . . . 13
5756adantr 465 . . . . . . . . . . . 12
58 fveq2 5871 . . . . . . . . . . . . 13
59 csbeq1 3437 . . . . . . . . . . . . . 14
60 csbeq1 3437 . . . . . . . . . . . . . 14
6159, 60difeq12d 3622 . . . . . . . . . . . . 13
6258, 61eleq12d 2539 . . . . . . . . . . . 12
6357, 62syl5ibrcom 222 . . . . . . . . . . 11
6463imp 429 . . . . . . . . . 10
65 nfv 1707 . . . . . . . . . . . . . . 15
66 nfcsb1v 3450 . . . . . . . . . . . . . . . 16
6766nfel2 2637 . . . . . . . . . . . . . . 15
68 fveq2 5871 . . . . . . . . . . . . . . . 16
69 csbeq1a 3443 . . . . . . . . . . . . . . . 16
7068, 69eleq12d 2539 . . . . . . . . . . . . . . 15
7165, 67, 70cbvral 3080 . . . . . . . . . . . . . 14
7226, 71sylib 196 . . . . . . . . . . . . 13
7372ad2antlr 726 . . . . . . . . . . . 12
7473r19.21bi 2826 . . . . . . . . . . 11
7574adantr 465 . . . . . . . . . 10
7620, 21, 64, 75ifbothda 3976 . . . . . . . . 9
7776ralrimiva 2871 . . . . . . . 8
78 simplll 759 . . . . . . . . 9
79 simpll 753 . . . . . . . . . . 11
80 iftrue 3947 . . . . . . . . . . . . . 14
8180, 61eqtrd 2498 . . . . . . . . . . . . 13
8258, 81eleq12d 2539 . . . . . . . . . . . 12
8382rspcva 3208 . . . . . . . . . . 11
8479, 83sylan 471 . . . . . . . . . 10
8584eldifbd 3488 . . . . . . . . 9
86 iftrue 3947 . . . . . . . . . . . . 13
8786, 43eqtrd 2498 . . . . . . . . . . . 12
8835, 87eleq12d 2539 . . . . . . . . . . 11
8988notbid 294 . . . . . . . . . 10
9089rspcev 3210 . . . . . . . . 9
9178, 85, 90syl2anc 661 . . . . . . . 8
9277, 91impbida 832 . . . . . . 7
93 nfv 1707 . . . . . . . 8
94 nfv 1707 . . . . . . . . . . 11
95 nfcsb1v 3450 . . . . . . . . . . 11
9694, 95, 28nfif 3970 . . . . . . . . . 10
9796nfel2 2637 . . . . . . . . 9
9897nfn 1901 . . . . . . . 8
99 eqeq1 2461 . . . . . . . . . . 11
100 csbeq1a 3443 . . . . . . . . . . 11
10199, 100, 31ifbieq12d 3968 . . . . . . . . . 10
10230, 101eleq12d 2539 . . . . . . . . 9
103102notbid 294 . . . . . . . 8
10493, 98, 103cbvrex 3081 . . . . . . 7
105 nfv 1707 . . . . . . . 8
106 nfv 1707 . . . . . . . . . 10
107 nfcsb1v 3450 . . . . . . . . . . 11
10866, 107nfdif 3624 . . . . . . . . . 10
109106, 108, 66nfif 3970 . . . . . . . . 9
110109nfel2 2637 . . . . . . . 8
111 eqeq1 2461 . . . . . . . . . 10
112 csbeq1a 3443 . . . . . . . . . . 11
11369, 112difeq12d 3622 . . . . . . . . . 10
114111, 113, 69ifbieq12d 3968 . . . . . . . . 9
11568, 114eleq12d 2539 . . . . . . . 8
116105, 110, 115cbvral 3080 . . . . . . 7
11792, 104, 1163bitr4g 288 . . . . . 6
11819, 117syl5bbr 259 . . . . 5
11918, 118bitrd 253 . . . 4
120 ibar 504 . . . . 5
121120adantl 466 . . . 4
12213biantrurd 508 . . . 4
123119, 121, 1223bitr3d 283 . . 3
124 eldif 3485 . . 3
12515elixp 7496 . . 3
126123, 124, 1253bitr4g 288 . 2
1272, 11, 126eqrdav 2455 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  A.wral 2807  E.wrex 2808  [_csb 3434  \cdif 3472  C_wss 3475  ifcif 3941  Fnwfn 5588  `cfv 5593  X_cixp 7489
This theorem is referenced by:  ptcld  20114
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fn 5596  df-fv 5601  df-ixp 7490
  Copyright terms: Public domain W3C validator