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

Theorem fneq1 5415
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 5356 . . 3  |-  ( F  =  G  ->  ( Fun  F  <->  Fun  G ) )
2 dmeq 4961 . . . 4  |-  ( F  =  G  ->  dom  F  =  dom  G )
32eqeq1d 2366 . . 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 5340 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
6 df-fn 5340 . 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 1642   dom cdm 4771   Fun wfun 5331    Fn wfn 5332
This theorem is referenced by:  fneq1d  5417  fneq1i  5420  fn0  5445  feq1  5457  foeq1  5530  f1ocnv  5568  dffn5  5651  mpteqb  5697  fnpr  5816  fnprOLD  5817  eufnfv  5838  tfrlem3  6480  tfrlem3a  6481  tfrlem12  6492  mapval2  6885  elixp2  6908  ixpfn  6910  elixpsn  6943  inf3lem6  7424  aceq3lem  7837  dfac4  7839  dfacacn  7857  axcc2lem  8152  axcc3  8154  seqof  11195  elpt  17373  elptr  17374  ptcmplem3  17850  prdsxmslem2  18177  feqmptdf  23279  wfrlem1  24814  wfrlem15  24828  frrlem1  24839  bpolyval  25343  fnchoice  27023  dfafn5b  27349  bnj62  28508  bnj976  28571  bnj66  28654  bnj124  28665  bnj607  28710  bnj873  28718  bnj1234  28805  bnj1463  28847
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4105  df-opab 4159  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-fun 5339  df-fn 5340
  Copyright terms: Public domain W3C validator