| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Membership relation for the values of a function whose image is a subclass. (Contributed by Raph Levien, 20-Nov-2006.) |
| Ref | Expression |
|---|---|
| funimass4 |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ssel 2615 |
. . . . . . . . . . . 12
| |
| 2 | visset 2295 |
. . . . . . . . . . . . . 14
| |
| 3 | 2 | funbrfvb 4714 |
. . . . . . . . . . . . 13
|
| 4 | 3 | ex 402 |
. . . . . . . . . . . 12
|
| 5 | 1, 4 | syl9 71 |
. . . . . . . . . . 11
|
| 6 | 5 | imp31 389 |
. . . . . . . . . 10
|
| 7 | eqcom 1886 |
. . . . . . . . . 10
| |
| 8 | 6, 7 | syl5bb 591 |
. . . . . . . . 9
|
| 9 | 8 | rexbidva 2120 |
. . . . . . . 8
|
| 10 | 2 | elima 4270 |
. . . . . . . 8
|
| 11 | 9, 10 | syl6rbbr 598 |
. . . . . . 7
|
| 12 | 11 | imbi1d 675 |
. . . . . 6
|
| 13 | r19.23v 2208 |
. . . . . 6
| |
| 14 | 12, 13 | syl6bbr 597 |
. . . . 5
|
| 15 | 14 | albidv 1656 |
. . . 4
|
| 16 | ralcom4 2310 |
. . . . 5
| |
| 17 | fvex 4689 |
. . . . . . 7
| |
| 18 | eleq1 1957 |
. . . . . . 7
| |
| 19 | 17, 18 | ceqsalv 2317 |
. . . . . 6
|
| 20 | 19 | ralbii 2127 |
. . . . 5
|
| 21 | 16, 20 | bitr3i 192 |
. . . 4
|
| 22 | 15, 21 | syl6bb 595 |
. . 3
|
| 23 | dfss2 2610 |
. . 3
| |
| 24 | 22, 23 | syl5bb 591 |
. 2
|
| 25 | 24 | ancoms 484 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: funimass3 4779 funimass5 4780 funconstss 4781 fipreima 10175 tx1cn 10223 tx2cn 10224 tartarmap 15265 fipreimaOLD 15756 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 1304 ax-gen 1305 ax-8 1306 ax-9 1307 ax-10 1308 ax-11 1309 ax-12 1310 ax-13 1311 ax-14 1312 ax-17 1317 ax-4 1319 ax-5o 1321 ax-6o 1324 ax-9o 1481 ax-10o 1500 ax-16 1580 ax-11o 1588 ax-ext 1865 ax-sep 3438 ax-nul 3445 ax-pow 3481 ax-pr 3524 ax-un 3790 |
| This theorem depends on definitions: df-bi 164 df-or 241 df-an 242 df-ex 1327 df-sb 1536 df-eu 1775 df-mo 1776 df-clab 1872 df-cleq 1877 df-clel 1880 df-ne 2019 df-ral 2109 df-rex 2110 df-v 2294 df-dif 2597 df-un 2600 df-in 2603 df-ss 2605 df-nul 2876 df-pw 3035 df-sn 3049 df-pr 3050 df-op 3053 df-uni 3178 df-br 3339 df-opab 3396 df-id 3586 df-xp 4000 df-cnv 4002 df-co 4003 df-dm 4004 df-rn 4005 df-res 4006 df-ima 4007 df-fun 4008 df-fn 4009 df-fv 4014 |