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

Theorem fneq1 5496
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 5434 . . 3  |-  ( F  =  G  ->  ( Fun  F  <->  Fun  G ) )
2 dmeq 5036 . . . 4  |-  ( F  =  G  ->  dom  F  =  dom  G )
32eqeq1d 2449 . . 3  |-  ( F  =  G  ->  ( dom  F  =  A  <->  dom  G  =  A ) )
41, 3anbi12d 705 . 2  |-  ( F  =  G  ->  (
( Fun  F  /\  dom  F  =  A )  <-> 
( Fun  G  /\  dom  G  =  A ) ) )
5 df-fn 5418 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
6 df-fn 5418 . 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 1364   dom cdm 4836   Fun wfun 5409    Fn wfn 5410
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-fun 5417  df-fn 5418
This theorem is referenced by:  fneq1d  5498  fneq1i  5502  fn0  5527  feq1  5539  foeq1  5613  f1ocnv  5650  dffn5  5734  mpteqb  5785  fnsnb  5895  fnprb  5933  fnprOLD  5934  eufnfv  5948  tfrlem12  6844  mapval2  7238  elixp2  7263  ixpfn  7265  elixpsn  7298  inf3lem6  7835  aceq3lem  8286  dfac4  8288  dfacacn  8306  axcc2lem  8601  axcc3  8603  seqof  11859  ccatvalfn  12276  swrdvalfn  12328  cshword  12424  0csh0  12426  rrgsupp  17340  elpt  19045  elptr  19046  ptcmplem3  19526  prdsxmslem2  20004  wfrlem1  27637  wfrlem15  27651  frrlem1  27681  fnchoice  29660  dfafn5b  29976  bnj62  31526  bnj976  31588  bnj66  31670  bnj124  31681  bnj607  31726  bnj873  31734  bnj1234  31821  bnj1463  31863
  Copyright terms: Public domain W3C validator