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

Theorem fneq1 5537
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 5476 . . 3  |-  ( F  =  G  ->  ( Fun  F  <->  Fun  G ) )
2 dmeq 5073 . . . 4  |-  ( F  =  G  ->  dom  F  =  dom  G )
32eqeq1d 2446 . . 3  |-  ( F  =  G  ->  ( dom  F  =  A  <->  dom  G  =  A ) )
41, 3anbi12d 693 . 2  |-  ( F  =  G  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  G  /\  dom  G  =  A ) ) )
5 df-fn 5460 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
6 df-fn 5460 . 2  |-  ( G  Fn  A  <->  ( Fun  G  /\  dom  G  =  A ) )
74, 5, 63bitr4g 281 1  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653   dom cdm 4881   Fun wfun 5451    Fn wfn 5452
This theorem is referenced by:  fneq1d  5539  fneq1i  5542  fn0  5567  feq1  5579  foeq1  5652  f1ocnv  5690  dffn5  5775  mpteqb  5822  fnpr  5953  fnprOLD  5954  eufnfv  5975  tfrlem3  6641  tfrlem3a  6642  tfrlem12  6653  mapval2  7046  elixp2  7069  ixpfn  7071  elixpsn  7104  inf3lem6  7591  aceq3lem  8006  dfac4  8008  dfacacn  8026  axcc2lem  8321  axcc3  8323  seqof  11385  elpt  17609  elptr  17610  ptcmplem3  18090  prdsxmslem2  18564  wfrlem1  25543  wfrlem15  25557  frrlem1  25587  fnchoice  27690  dfafn5b  28015  ccatvalfn  28210  swrdvalfn  28220  cshword  28269  bnj62  29159  bnj976  29222  bnj66  29305  bnj124  29316  bnj607  29361  bnj873  29369  bnj1234  29456  bnj1463  29498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rab 2716  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-br 4216  df-opab 4270  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-fun 5459  df-fn 5460
  Copyright terms: Public domain W3C validator