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

Theorem fneq1 5675
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 5613 . . 3  |-  ( F  =  G  ->  ( Fun  F  <->  Fun  G ) )
2 dmeq 5209 . . . 4  |-  ( F  =  G  ->  dom  F  =  dom  G )
32eqeq1d 2469 . . 3  |-  ( F  =  G  ->  ( dom  F  =  A  <->  dom  G  =  A ) )
41, 3anbi12d 710 . 2  |-  ( F  =  G  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  G  /\  dom  G  =  A ) ) )
5 df-fn 5597 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
6 df-fn 5597 . 2  |-  ( G  Fn  A  <->  ( Fun  G  /\  dom  G  =  A ) )
74, 5, 63bitr4g 288 1  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   dom cdm 5005   Fun wfun 5588    Fn wfn 5589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-op 4040  df-br 4454  df-opab 4512  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-fun 5596  df-fn 5597
This theorem is referenced by:  fneq1d  5677  fneq1i  5681  fn0  5706  feq1  5719  foeq1  5797  f1ocnv  5834  dffn5  5919  mpteqb  5971  fnsnb  6091  fnprb  6130  fnprOLD  6131  eufnfv  6145  tfrlem12  7070  mapval2  7460  elixp2  7485  ixpfn  7487  elixpsn  7520  inf3lem6  8062  aceq3lem  8513  dfac4  8515  dfacacn  8533  axcc2lem  8828  axcc3  8830  seqof  12144  ccatvalfn  12579  swrdvalfn  12643  cshword  12742  0csh0  12744  rrgsupp  17809  elpt  19941  elptr  19942  ptcmplem3  20422  prdsxmslem2  20900  wfrlem1  29270  wfrlem15  29284  frrlem1  29314  fnchoice  31306  fourierdlem42  31772  dfafn5b  32036  bnj62  33254  bnj976  33316  bnj66  33398  bnj124  33409  bnj607  33454  bnj873  33462  bnj1234  33549  bnj1463  33591
  Copyright terms: Public domain W3C validator