Mathbox for Scott Fenton < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brrestrict Structured version   Unicode version

Theorem brrestrict 25796
 Description: The binary relationship form of the Restrict function. (Contributed by Scott Fenton, 17-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Hypotheses
Ref Expression
brrestrict.1
brrestrict.2
brrestrict.3
Assertion
Ref Expression
brrestrict Restrict

Proof of Theorem brrestrict
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 4429 . . . . 5
2 brrestrict.3 . . . . 5
31, 2brco 5045 . . . 4 Cap Cart Range Cart Range Cap
41brtxp2 25728 . . . . . . 7 Cart Range Cart Range
5 3anrot 942 . . . . . . . . 9 Cart Range Cart Range
6 brrestrict.1 . . . . . . . . . . 11
7 brrestrict.2 . . . . . . . . . . 11
8 vex 2961 . . . . . . . . . . 11
96, 7, 8br1steq 25400 . . . . . . . . . 10
10 vex 2961 . . . . . . . . . . . 12
111, 10brco 5045 . . . . . . . . . . 11 Cart Range Range Cart
121brtxp2 25728 . . . . . . . . . . . . . . 15 Range Range
13 3anrot 942 . . . . . . . . . . . . . . . . 17 Range Range
146, 7, 8br2ndeq 25401 . . . . . . . . . . . . . . . . . 18
151, 10brco 5045 . . . . . . . . . . . . . . . . . . 19 Range Range
16 vex 2961 . . . . . . . . . . . . . . . . . . . . . . 23
176, 7, 16br1steq 25400 . . . . . . . . . . . . . . . . . . . . . 22
1817anbi1i 678 . . . . . . . . . . . . . . . . . . . . 21 Range Range
1918exbii 1593 . . . . . . . . . . . . . . . . . . . 20 Range Range
20 breq1 4217 . . . . . . . . . . . . . . . . . . . . 21 Range Range
216, 20ceqsexv 2993 . . . . . . . . . . . . . . . . . . . 20 Range Range
2219, 21bitri 242 . . . . . . . . . . . . . . . . . . 19 Range Range
236, 10brrange 25781 . . . . . . . . . . . . . . . . . . 19 Range
2415, 22, 233bitri 264 . . . . . . . . . . . . . . . . . 18 Range
25 biid 229 . . . . . . . . . . . . . . . . . 18
2614, 24, 253anbi123i 1143 . . . . . . . . . . . . . . . . 17 Range
2713, 26bitri 242 . . . . . . . . . . . . . . . 16 Range
28272exbii 1594 . . . . . . . . . . . . . . 15 Range
296rnex 5135 . . . . . . . . . . . . . . . 16
30 opeq1 3986 . . . . . . . . . . . . . . . . 17
3130eqeq2d 2449 . . . . . . . . . . . . . . . 16
32 opeq2 3987 . . . . . . . . . . . . . . . . 17
3332eqeq2d 2449 . . . . . . . . . . . . . . . 16
347, 29, 31, 33ceqsex2v 2995 . . . . . . . . . . . . . . 15
3512, 28, 343bitri 264 . . . . . . . . . . . . . 14 Range
3635anbi1i 678 . . . . . . . . . . . . 13 Range Cart Cart
3736exbii 1593 . . . . . . . . . . . 12 Range Cart Cart
38 opex 4429 . . . . . . . . . . . . 13
39 breq1 4217 . . . . . . . . . . . . 13 Cart Cart
4038, 39ceqsexv 2993 . . . . . . . . . . . 12 Cart Cart
4137, 40bitri 242 . . . . . . . . . . 11 Range Cart Cart
427, 29, 10brcart 25779 . . . . . . . . . . 11 Cart
4311, 41, 423bitri 264 . . . . . . . . . 10 Cart Range
449, 43, 253anbi123i 1143 . . . . . . . . 9 Cart Range
455, 44bitri 242 . . . . . . . 8 Cart Range
46452exbii 1594 . . . . . . 7 Cart Range
477, 29xpex 4992 . . . . . . . 8
48 opeq1 3986 . . . . . . . . 9
4948eqeq2d 2449 . . . . . . . 8
50 opeq2 3987 . . . . . . . . 9
5150eqeq2d 2449 . . . . . . . 8
526, 47, 49, 51ceqsex2v 2995 . . . . . . 7
534, 46, 523bitri 264 . . . . . 6 Cart Range
5453anbi1i 678 . . . . 5 Cart Range Cap Cap
5554exbii 1593 . . . 4 Cart Range Cap Cap
563, 55bitri 242 . . 3 Cap Cart Range Cap
57 opex 4429 . . . 4
58 breq1 4217 . . . 4 Cap Cap
5957, 58ceqsexv 2993 . . 3 Cap Cap
606, 47, 2brcap 25787 . . 3 Cap
6156, 59, 603bitri 264 . 2 Cap Cart Range
62 df-restrict 25717 . . 3 Restrict Cap Cart Range
6362breqi 4220 . 2 Restrict Cap Cart Range
64 dfres3 25384 . . 3
6564eqeq2i 2448 . 2
6661, 63, 653bitr4i 270 1 Restrict
 Colors of variables: wff set class Syntax hints:   wb 178   wa 360   w3a 937  wex 1551   wceq 1653   wcel 1726  cvv 2958   cin 3321  cop 3819   class class class wbr 4214   cxp 4878   crn 4881   cres 4882   ccom 4884  c1st 6349  c2nd 6350   ctxp 25676  Cartccart 25687  Rangecrange 25690  Capccap 25693  Restrictcrestrict 25697 This theorem is referenced by:  tfrqfree  25798 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4215  df-opab 4269  df-mpt 4270  df-eprel 4496  df-id 4500  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-fo 5462  df-fv 5464  df-1st 6351  df-2nd 6352  df-symdif 25665  df-txp 25700  df-pprod 25701  df-image 25710  df-cart 25711  df-range 25714  df-cap 25716  df-restrict 25717
 Copyright terms: Public domain W3C validator