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

Theorem fneq1 5493
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 5432 . . 3  |-  ( F  =  G  ->  ( Fun  F  <->  Fun  G ) )
2 dmeq 5029 . . . 4  |-  ( F  =  G  ->  dom  F  =  dom  G )
32eqeq1d 2412 . . 3  |-  ( F  =  G  ->  ( dom  F  =  A  <->  dom  G  =  A ) )
41, 3anbi12d 692 . 2  |-  ( F  =  G  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  G  /\  dom  G  =  A ) ) )
5 df-fn 5416 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
6 df-fn 5416 . 2  |-  ( G  Fn  A  <->  ( Fun  G  /\  dom  G  =  A ) )
74, 5, 63bitr4g 280 1  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649   dom cdm 4837   Fun wfun 5407    Fn wfn 5408
This theorem is referenced by:  fneq1d  5495  fneq1i  5498  fn0  5523  feq1  5535  foeq1  5608  f1ocnv  5646  dffn5  5731  mpteqb  5778  fnpr  5909  fnprOLD  5910  eufnfv  5931  tfrlem3  6597  tfrlem3a  6598  tfrlem12  6609  mapval2  7002  elixp2  7025  ixpfn  7027  elixpsn  7060  inf3lem6  7544  aceq3lem  7957  dfac4  7959  dfacacn  7977  axcc2lem  8272  axcc3  8274  seqof  11335  elpt  17557  elptr  17558  ptcmplem3  18038  prdsxmslem2  18512  wfrlem1  25470  wfrlem15  25484  frrlem1  25495  bpolyval  25999  fnchoice  27567  dfafn5b  27892  swrdvalfn  28007  ccatvalfn  28008  bnj62  28791  bnj976  28854  bnj66  28937  bnj124  28948  bnj607  28993  bnj873  29001  bnj1234  29088  bnj1463  29130
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-fun 5415  df-fn 5416
  Copyright terms: Public domain W3C validator