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

Theorem frnsuppeq 6929
 Description: Two ways of writing the support of a function with known codomain. (Contributed by Stefan O'Rear, 9-Jul-2015.) (Revised by AV, 7-Jul-2019.)
Assertion
Ref Expression
frnsuppeq supp

Proof of Theorem frnsuppeq
StepHypRef Expression
1 fex 6146 . . . . . . 7
21expcom 435 . . . . . 6
32adantr 465 . . . . 5
43imp 429 . . . 4
5 simplr 755 . . . 4
6 suppimacnv 6928 . . . 4 supp
74, 5, 6syl2anc 661 . . 3 supp
8 invdif 3746 . . . . . 6
98imaeq2i 5345 . . . . 5
10 ffun 5739 . . . . . . 7
11 inpreima 6015 . . . . . . 7
1210, 11syl 16 . . . . . 6
13 cnvimass 5367 . . . . . . . 8
14 fdm 5741 . . . . . . . . 9
15 fimacnv 6020 . . . . . . . . 9
1614, 15eqtr4d 2501 . . . . . . . 8
1713, 16syl5sseq 3547 . . . . . . 7
18 sseqin2 3713 . . . . . . 7
1917, 18sylib 196 . . . . . 6
2012, 19eqtrd 2498 . . . . 5
219, 20syl5reqr 2513 . . . 4