![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > suppssfvOLD | Unicode version |
Description: Formula building theorem for support restriction, on a function which preserves zero. (Contributed by Stefan O'Rear, 9-Mar-2015.) Obsolete version of suppssfv 6955 as of 28-May-2019. (New usage is discouraged.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
suppssfvOLD.a | |
suppssfvOLD.f | |
suppssfvOLD.v |
Ref | Expression |
---|---|
suppssfvOLD |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifsni 4156 | . . . . 5 | |
2 | suppssfvOLD.v | . . . . . . . . 9 | |
3 | elex 3118 | . . . . . . . . 9 | |
4 | 2, 3 | syl 16 | . . . . . . . 8 |
5 | 4 | adantr 465 | . . . . . . 7 |
6 | suppssfvOLD.f | . . . . . . . . . . 11 | |
7 | fveq2 5871 | . . . . . . . . . . . 12 | |
8 | 7 | eqeq1d 2459 | . . . . . . . . . . 11 |
9 | 6, 8 | syl5ibrcom 222 | . . . . . . . . . 10 |
10 | 9 | necon3d 2681 | . . . . . . . . 9 |
11 | 10 | adantr 465 | . . . . . . . 8 |
12 | 11 | imp 429 | . . . . . . 7 |
13 | eldifsn 4155 | . . . . . . 7 | |
14 | 5, 12, 13 | sylanbrc 664 | . . . . . 6 |
15 | 14 | ex 434 | . . . . 5 |
16 | 1, 15 | syl5 32 | . . . 4 |
17 | 16 | ss2rabdv 3580 | . . 3 |
18 | eqid 2457 | . . . 4 | |
19 | 18 | mptpreima 5505 | . . 3 |
20 | eqid 2457 | . . . 4 | |
21 | 20 | mptpreima 5505 | . . 3 |
22 | 17, 19, 21 | 3sstr4g 3544 | . 2 |
23 | suppssfvOLD.a | . 2 | |
24 | 22, 23 | sstrd 3513 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -> wi 4 /\ wa 369
= wceq 1395 e. wcel 1818 =/= wne 2652
{ crab 2811 cvv 3109
\ cdif 3472 C_ wss 3475 { csn 4029
e. cmpt 4510 `' ccnv 5003 " cima 5007
` cfv 5593 |
This theorem is referenced by: evlslem6OLD 18182 |
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-9 1822 ax-10 1837 ax-11 1842 ax-12 1854 ax-13 1999 ax-ext 2435 ax-sep 4573 ax-nul 4581 ax-pr 4691 |
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-eu 2286 df-mo 2287 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-ral 2812 df-rex 2813 df-rab 2816 df-v 3111 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-mpt 4512 df-xp 5010 df-rel 5011 df-cnv 5012 df-dm 5014 df-rn 5015 df-res 5016 df-ima 5017 df-iota 5556 df-fv 5601 |
Copyright terms: Public domain | W3C validator |