Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  afvres Unicode version

Theorem afvres 29752
Description: The value of a restricted function, analogous to fvres 5674. (Contributed by Alexander van der Vekens, 22-Jul-2017.)
Assertion
Ref Expression
afvres

Proof of Theorem afvres
StepHypRef Expression
1 elin 3516 . . . . . . . . 9
21biimpri 200 . . . . . . . 8
3 dmres 5103 . . . . . . . 8
42, 3syl6eleqr 2513 . . . . . . 7
54ex 427 . . . . . 6
6 snssi 3992 . . . . . . . . . 10
7 resabs1 5111 . . . . . . . . . 10
86, 7syl 16 . . . . . . . . 9
98eqcomd 2427 . . . . . . . 8
109funeqd 5411 . . . . . . 7
1110biimpd 201 . . . . . 6
125, 11anim12d 550 . . . . 5
1312impcom 423 . . . 4
14 df-dfat 29694 . . . . 5
15 afvfundmfveq 29718 . . . . 5
1614, 15sylbir 207 . . . 4
1713, 16syl 16 . . 3
18 fvres 5674 . . . 4
1918adantl 456 . . 3
20 df-dfat 29694 . . . . . 6
21 afvfundmfveq 29718 . . . . . 6
2220, 21sylbir 207 . . . . 5
2322eqcomd 2427 . . . 4
2423adantr 455 . . 3
2517, 19, 243eqtrd 2458 . 2
26 pm3.4 548 . . . . . . . . . 10
271, 26sylbi 189 . . . . . . . . 9
2827, 3eleq2s 2514 . . . . . . . 8
2928com12 30 . . . . . . 7
308funeqd 5411 . . . . . . . 8
3130biimpd 201 . . . . . . 7
3229, 31anim12d 550 . . . . . 6
3332con3d 128 . . . . 5
3433impcom 423 . . . 4
35 afvnfundmuv 29719 . . . . 5
3614, 35sylnbir 301 . . . 4
3734, 36syl 16 . . 3
38 afvnfundmuv 29719 . . . . . 6
3920, 38sylnbir 301 . . . . 5
4039eqcomd 2427 . . . 4
4140adantr 455 . . 3
4237, 41eqtrd 2454 . 2
4325, 42pm2.61ian 773 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 362  =wceq 1687  e.wcel 1749   cvv 2951  i^icin 3304  C_wss 3305  {csn 3853  domcdm 4811  |`cres 4813  Funwfun 5384  `cfv 5390   wdfat 29691   cafv 29692
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-opab 4326  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-res 4823  df-iota 5353  df-fun 5392  df-fv 5398  df-dfat 29694  df-afv 29695
  Copyright terms: Public domain W3C validator