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

Theorem fneq1 5333
Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fneq1  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )

Proof of Theorem fneq1
StepHypRef Expression
1 funeq 5274 . . 3  |-  ( F  =  G  ->  ( Fun  F  <->  Fun  G ) )
2 dmeq 4879 . . . 4  |-  ( F  =  G  ->  dom  F  =  dom  G )
32eqeq1d 2291 . . 3  |-  ( F  =  G  ->  ( dom  F  =  A  <->  dom  G  =  A ) )
41, 3anbi12d 691 . 2  |-  ( F  =  G  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  G  /\  dom  G  =  A ) ) )
5 df-fn 5258 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
6 df-fn 5258 . 2  |-  ( G  Fn  A  <->  ( Fun  G  /\  dom  G  =  A ) )
74, 5, 63bitr4g 279 1  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623   dom cdm 4689   Fun wfun 5249    Fn wfn 5250
This theorem is referenced by:  fneq1d  5335  fneq1i  5338  fn0  5363  feq1  5375  foeq1  5447  f1ocnv  5485  dffn5  5568  mpteqb  5614  eufnfv  5752  tfrlem3  6393  tfrlem3a  6394  tfrlem12  6405  mapval2  6797  elixp2  6820  ixpfn  6822  elixpsn  6855  inf3lem6  7334  aceq3lem  7747  dfac4  7749  dfacacn  7767  axcc2lem  8062  axcc3  8064  seqof  11103  elpt  17267  elptr  17268  ptcmplem3  17748  prdsxmslem2  18075  feqmptdf  23228  wfrlem1  24256  wfrlem15  24270  frrlem1  24281  bpolyval  24784  repfuntw  25160  repcpwti  25161  fnchoice  27700  dfafn5b  28023  bnj62  28746  bnj976  28809  bnj66  28892  bnj124  28903  bnj607  28948  bnj873  28956  bnj1234  29043  bnj1463  29085
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-fun 5257  df-fn 5258
  Copyright terms: Public domain W3C validator