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

Theorem fnsuppresOLD 6132
 Description: Two ways to express restriction of a support set. (Contributed by Stefan O'Rear, 5-Feb-2015.) Obsolete version of fnsuppres 6945 as of 28-May-2019. (New usage is discouraged.) (Proof modification is discouraged.)
Assertion
Ref Expression
fnsuppresOLD

Proof of Theorem fnsuppresOLD
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 unss 3674 . . . 4
2 ssrab2 3581 . . . . 5
32biantrur 506 . . . 4
4 rabun2 3784 . . . . 5
54sseq1i 3523 . . . 4
61, 3, 53bitr4ri 278 . . 3
7 rabss 3573 . . . 4
8 fvres 5886 . . . . . . . 8
98adantl 466 . . . . . . 7
10 fvconst2g 6126 . . . . . . . 8
11103ad2antl3 1160 . . . . . . 7
129, 11eqeq12d 2479 . . . . . 6
13 nne 2658 . . . . . . 7
1413a1i 11 . . . . . 6
15 id 22 . . . . . . . 8
16 simp2 997 . . . . . . . 8
17 minel 3885 . . . . . . . 8
1815, 16, 17syl2anr 478 . . . . . . 7
19 mtt 339 . . . . . . 7
2018, 19syl 16 . . . . . 6
2112, 14, 203bitr2rd 282 . . . . 5
2221ralbidva 2893 . . . 4
237, 22syl5bb 257 . . 3
246, 23syl5bb 257 . 2
25 fnniniseg2OLD 6012 . . . 4