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

Theorem fneq1 5610
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 5548 . . 3  |-  ( F  =  G  ->  ( Fun  F  <->  Fun  G ) )
2 dmeq 5151 . . . 4  |-  ( F  =  G  ->  dom  F  =  dom  G )
32eqeq1d 2456 . . 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 5532 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
6 df-fn 5532 . 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 1370   dom cdm 4951   Fun wfun 5523    Fn wfn 5524
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-br 4404  df-opab 4462  df-rel 4958  df-cnv 4959  df-co 4960  df-dm 4961  df-fun 5531  df-fn 5532
This theorem is referenced by:  fneq1d  5612  fneq1i  5616  fn0  5641  feq1  5653  foeq1  5727  f1ocnv  5764  dffn5  5849  mpteqb  5900  fnsnb  6010  fnprb  6048  fnprOLD  6049  eufnfv  6063  tfrlem12  6961  mapval2  7355  elixp2  7380  ixpfn  7382  elixpsn  7415  inf3lem6  7954  aceq3lem  8405  dfac4  8407  dfacacn  8425  axcc2lem  8720  axcc3  8722  seqof  11984  ccatvalfn  12402  swrdvalfn  12454  cshword  12550  0csh0  12552  rrgsupp  17495  elpt  19287  elptr  19288  ptcmplem3  19768  prdsxmslem2  20246  wfrlem1  27891  wfrlem15  27905  frrlem1  27935  fnchoice  29922  dfafn5b  30238  bnj62  32064  bnj976  32126  bnj66  32208  bnj124  32219  bnj607  32264  bnj873  32272  bnj1234  32359  bnj1463  32401
  Copyright terms: Public domain W3C validator