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

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

Proof of Theorem brimg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opex 4385 . . . 4
2 brimg.3 . . . 4
31, 2brco 5000 . . 3 Image Cart Cart Image
4 brimg.1 . . . . . 6
5 brimg.2 . . . . . 6
6 vex 2917 . . . . . 6
74, 5, 6brcart 25683 . . . . 5 Cart
87anbi1i 677 . . . 4 Cart Image Image
98exbii 1589 . . 3 Cart Image Image
104, 5xpex 4947 . . . . 5
11 breq1 4173 . . . . 5 Image Image
1210, 11ceqsexv 2949 . . . 4 Image Image
1310, 2brimage 25677 . . . 4 Image
1412, 13bitri 241 . . 3 Image
153, 9, 143bitri 263 . 2 Image Cart
16 df-img 25619 . . 3 Img Image Cart
1716breqi 4176 . 2 Img Image Cart
18 df-rex 2670 . . . . . 6
19 elxp 4852 . . . . . . . . 9
2019anbi1i 677 . . . . . . . 8
21 19.41vv 1921 . . . . . . . 8
22 anass 631 . . . . . . . . 9
23222exbii 1590 . . . . . . . 8
2420, 21, 233bitr2i 265 . . . . . . 7
2524exbii 1589 . . . . . 6
26 excom 1752 . . . . . . 7
27 excom 1752 . . . . . . . . 9
28 opex 4385 . . . . . . . . . . 11
29 breq1 4173 . . . . . . . . . . . . 13
306brres 5109 . . . . . . . . . . . . . 14
31 vex 2917 . . . . . . . . . . . . . . . . 17
3231brres 5109 . . . . . . . . . . . . . . . 16
33 df-br 4171 . . . . . . . . . . . . . . . 16
34 ancom 438 . . . . . . . . . . . . . . . . 17
35 19.41vv 1921 . . . . . . . . . . . . . . . . 17
36 elvv 4893 . . . . . . . . . . . . . . . . . 18
3736anbi2i 676 . . . . . . . . . . . . . . . . 17
3834, 35, 373bitr4ri 270 . . . . . . . . . . . . . . . 16
3932, 33, 383bitr3i 267 . . . . . . . . . . . . . . 15
4039anbi2i 676 . . . . . . . . . . . . . 14
4130, 40bitr2i 242 . . . . . . . . . . . . 13
4229, 41syl6bbr 255 . . . . . . . . . . . 12
4342anbi2d 685 . . . . . . . . . . 11
4428, 43ceqsexv 2949 . . . . . . . . . 10
4544exbii 1589 . . . . . . . . 9
4627, 45bitri 241 . . . . . . . 8
4746exbii 1589 . . . . . . 7
48 an12 773 . . . . . . . . . 10
49482exbii 1590 . . . . . . . . 9
50492exbii 1590 . . . . . . . 8
51 19.42vv 1926 . . . . . . . . . 10
52 anass 631 . . . . . . . . . 10
5351, 52bitri 241 . . . . . . . . 9
54532exbii 1590 . . . . . . . 8
55 exrot3 1755 . . . . . . . . . 10
5655exbii 1589 . . . . . . . . 9
57 exrot3 1755 . . . . . . . . 9
58 exdistr 1925 . . . . . . . . . . . 12
59 opex 4385 . . . . . . . . . . . . 13
60 eleq1 2462 . . . . . . . . . . . . . . . . 17
6160anbi1d 686 . . . . . . . . . . . . . . . 16
62 opeq1 3942 . . . . . . . . . . . . . . . . 17
6362breq1d 4180 . . . . . . . . . . . . . . . 16
6461, 63anbi12d 692 . . . . . . . . . . . . . . 15
65 breq1 4173 . . . . . . . . . . . . . . . 16
66 vex 2917 . . . . . . . . . . . . . . . . 17
67 vex 2917 . . . . . . . . . . . . . . . . 17
6866, 67, 31br1steq 25342 . . . . . . . . . . . . . . . 16
6965, 68syl6bb 253 . . . . . . . . . . . . . . 15
7064, 69anbi12d 692 . . . . . . . . . . . . . 14
7170exbidv 1633 . . . . . . . . . . . . 13
7259, 71ceqsexv 2949 . . . . . . . . . . . 12
7358, 72bitri 241 . . . . . . . . . . 11
74732exbii 1590 . . . . . . . . . 10
75 exancom 1593 . . . . . . . . . . . 12
76 eleq1 2462 . . . . . . . . . . . . . . 15
7776anbi2d 685 . . . . . . . . . . . . . 14
78 opeq2 3943 . . . . . . . . . . . . . . 15
7978breq1d 4180 . . . . . . . . . . . . . 14
8077, 79anbi12d 692 . . . . . . . . . . . . 13
8166, 80ceqsexv 2949 . . . . . . . . . . . 12
8275, 81bitri 241 . . . . . . . . . . 11
83822exbii 1590 . . . . . . . . . 10
84 exdistr 1925 . . . . . . . . . . 11
85 an32 774 . . . . . . . . . . . . 13
86 ancom 438 . . . . . . . . . . . . 13
8785, 86bitri 241 . . . . . . . . . . . 12
88872exbii 1590 . . . . . . . . . . 11
89 df-rex 2670 . . . . . . . . . . 11
9084, 88, 893bitr4i 269 . . . . . . . . . 10
9174, 83, 903bitri 263 . . . . . . . . 9
9256, 57, 913bitri 263 . . . . . . . 8
9350, 54, 923bitr3i 267 . . . . . . 7
9426, 47, 933bitri 263 . . . . . 6
9518, 25, 943bitri 263 . . . . 5
966elima 5165 . . . . 5
976elima 5165 . . . . . 6
98 opeq2 3943 . . . . . . . . . 10
9998eleq1d 2468 . . . . . . . . 9
1006, 99ceqsexv 2949 . . . . . . . 8
101 ancom 438 . . . . . . . . . 10
102 opex 4385 . . . . . . . . . . . . 13
103102, 6brco 5000 . . . . . . . . . . . 12
104 vex 2917 . . . . . . . . . . . . . . 15
10559, 66, 104br1steq 25342 . . . . . . . . . . . . . 14
106105anbi1i 677 . . . . . . . . . . . . 13
107106exbii 1589 . . . . . . . . . . . 12
108 breq1 4173 . . . . . . . . . . . . . 14
10959, 108ceqsexv 2949 . . . . . . . . . . . . 13
11066, 67, 6br2ndeq 25343 . . . . . . . . . . . . 13
111 equcom 1688 . . . . . . . . . . . . 13
112109, 110, 1113bitri 263 . . . . . . . . . . . 12
113103, 107, 1123bitri 263 . . . . . . . . . . 11
114113anbi1i 677 . . . . . . . . . 10
115101, 114bitri 241 . . . . . . . . 9
116115exbii 1589 . . . . . . . 8
117 df-br 4171 . . . . . . . 8
118100, 116, 1173bitr4ri 270 . . . . . . 7
119118rexbii 2689 . . . . . 6
12097, 119bitri 241 . . . . 5
12195, 96, 1203bitr4ri 270 . . . 4
122121eqriv 2399 . . 3
123122eqeq2i 2412 . 2
12415, 17, 1233bitr4i 269 1 Img
 Colors of variables: wff set class Syntax hints:   wb 177   wa 359  wex 1547   wceq 1649   wcel 1721  wrex 2665  cvv 2914  cop 3775   class class class wbr 4170   cxp 4833   cres 4837  cima 4838   ccom 4839  c1st 6304  c2nd 6305  Imagecimage 25595  Cartccart 25596  Imgcimg 25597 This theorem is referenced by:  brapply  25689  dfrdg4  25701 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2383  ax-sep 4288  ax-nul 4296  ax-pow 4335  ax-pr 4361  ax-un 4658 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2389  df-cleq 2395  df-clel 2398  df-nfc 2527  df-ne 2567  df-ral 2669  df-rex 2670  df-rab 2673  df-v 2916  df-sbc 3120  df-dif 3281  df-un 3283  df-in 3285  df-ss 3292  df-nul 3587  df-if 3698  df-pw 3759  df-sn 3778  df-pr 3779  df-op 3781  df-uni 3974  df-br 4171  df-opab 4225  df-mpt 4226  df-eprel 4452  df-id 4456  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5375  df-fun 5413  df-fn 5414  df-f 5415  df-fo 5417  df-fv 5419  df-1st 6306  df-2nd 6307  df-symdif 25574  df-txp 25607  df-pprod 25608  df-image 25617  df-cart 25618  df-img 25619
 Copyright terms: Public domain W3C validator