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

Theorem fvsnun2 5755
Description: The value of a function with one of its ordered pairs replaced, at arguments other than the replaced one. See also fvsnun1 5754. (Contributed by NM, 23-Sep-2007.)
Hypotheses
Ref Expression
fvsnun.1  |-  A  e. 
_V
fvsnun.2  |-  B  e. 
_V
fvsnun.3  |-  G  =  ( { <. A ,  B >. }  u.  ( F  |`  ( C  \  { A } ) ) )
Assertion
Ref Expression
fvsnun2  |-  ( D  e.  ( C  \  { A } )  -> 
( G `  D
)  =  ( F `
 D ) )

Proof of Theorem fvsnun2
StepHypRef Expression
1 fvsnun.3 . . . . 5  |-  G  =  ( { <. A ,  B >. }  u.  ( F  |`  ( C  \  { A } ) ) )
21reseq1i 4988 . . . 4  |-  ( G  |`  ( C  \  { A } ) )  =  ( ( { <. A ,  B >. }  u.  ( F  |`  ( C 
\  { A }
) ) )  |`  ( C  \  { A } ) )
3 resundir 5007 . . . 4  |-  ( ( { <. A ,  B >. }  u.  ( F  |`  ( C  \  { A } ) ) )  |`  ( C  \  { A } ) )  =  ( ( { <. A ,  B >. }  |`  ( C  \  { A }
) )  u.  (
( F  |`  ( C  \  { A }
) )  |`  ( C  \  { A }
) ) )
4 disjdif 3560 . . . . . . 7  |-  ( { A }  i^i  ( C  \  { A }
) )  =  (/)
5 fvsnun.1 . . . . . . . . 9  |-  A  e. 
_V
6 fvsnun.2 . . . . . . . . 9  |-  B  e. 
_V
75, 6fnsn 5341 . . . . . . . 8  |-  { <. A ,  B >. }  Fn  { A }
8 fnresdisj 5391 . . . . . . . 8  |-  ( {
<. A ,  B >. }  Fn  { A }  ->  ( ( { A }  i^i  ( C  \  { A } ) )  =  (/)  <->  ( { <. A ,  B >. }  |`  ( C  \  { A }
) )  =  (/) ) )
97, 8ax-mp 8 . . . . . . 7  |-  ( ( { A }  i^i  ( C  \  { A } ) )  =  (/) 
<->  ( { <. A ,  B >. }  |`  ( C  \  { A }
) )  =  (/) )
104, 9mpbi 199 . . . . . 6  |-  ( {
<. A ,  B >. }  |`  ( C  \  { A } ) )  =  (/)
11 residm 5023 . . . . . 6  |-  ( ( F  |`  ( C  \  { A } ) )  |`  ( C  \  { A } ) )  =  ( F  |`  ( C  \  { A } ) )
1210, 11uneq12i 3361 . . . . 5  |-  ( ( { <. A ,  B >. }  |`  ( C  \  { A } ) )  u.  ( ( F  |`  ( C  \  { A } ) )  |`  ( C  \  { A } ) ) )  =  (
(/)  u.  ( F  |`  ( C  \  { A } ) ) )
13 uncom 3353 . . . . 5  |-  ( (/)  u.  ( F  |`  ( C  \  { A }
) ) )  =  ( ( F  |`  ( C  \  { A } ) )  u.  (/) )
14 un0 3513 . . . . 5  |-  ( ( F  |`  ( C  \  { A } ) )  u.  (/) )  =  ( F  |`  ( C  \  { A }
) )
1512, 13, 143eqtri 2340 . . . 4  |-  ( ( { <. A ,  B >. }  |`  ( C  \  { A } ) )  u.  ( ( F  |`  ( C  \  { A } ) )  |`  ( C  \  { A } ) ) )  =  ( F  |`  ( C  \  { A } ) )
162, 3, 153eqtri 2340 . . 3  |-  ( G  |`  ( C  \  { A } ) )  =  ( F  |`  ( C  \  { A }
) )
1716fveq1i 5564 . 2  |-  ( ( G  |`  ( C  \  { A } ) ) `  D )  =  ( ( F  |`  ( C  \  { A } ) ) `  D )
18 fvres 5580 . 2  |-  ( D  e.  ( C  \  { A } )  -> 
( ( G  |`  ( C  \  { A } ) ) `  D )  =  ( G `  D ) )
19 fvres 5580 . 2  |-  ( D  e.  ( C  \  { A } )  -> 
( ( F  |`  ( C  \  { A } ) ) `  D )  =  ( F `  D ) )
2017, 18, 193eqtr3a 2372 1  |-  ( D  e.  ( C  \  { A } )  -> 
( G `  D
)  =  ( F `
 D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1633    e. wcel 1701   _Vcvv 2822    \ cdif 3183    u. cun 3184    i^i cin 3185   (/)c0 3489   {csn 3674   <.cop 3677    |` cres 4728    Fn wfn 5287   ` cfv 5292
This theorem is referenced by:  facnn  11337
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-opab 4115  df-id 4346  df-xp 4732  df-rel 4733  df-cnv 4734  df-co 4735  df-dm 4736  df-res 4738  df-iota 5256  df-fun 5294  df-fn 5295  df-fv 5300
  Copyright terms: Public domain W3C validator