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

Theorem fneq1 6140
Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fneq1 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))

Proof of Theorem fneq1
StepHypRef Expression
1 funeq 6069 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2 dmeq 5479 . . . 4 (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
32eqeq1d 2762 . . 3 (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
41, 3anbi12d 749 . 2 (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5 df-fn 6052 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6 df-fn 6052 . 2 (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
74, 5, 63bitr4g 303 1 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383   = wceq 1632  dom cdm 5266  Fun wfun 6043   Fn wfn 6044
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-fun 6051  df-fn 6052
This theorem is referenced by:  fneq1d  6142  fneq1i  6146  fn0  6172  feq1  6187  foeq1  6272  f1ocnv  6310  dffn5  6403  mpteqb  6461  fnsnb  6596  fnprb  6636  fntpb  6637  eufnfv  6654  wfrlem1  7583  wfrlem3a  7586  wfrlem15  7598  tfrlem12  7654  mapval2  8053  elixp2  8078  ixpfn  8080  elixpsn  8113  inf3lem6  8703  aceq3lem  9133  dfac4  9135  dfacacn  9155  axcc2lem  9450  axcc3  9452  seqof  13052  ccatvalfn  13553  cshword  13737  0csh0  13739  lmodfopnelem1  19101  rrgsupp  19493  elpt  21577  elptr  21578  ptcmplem3  22059  prdsxmslem2  22535  bnj62  31095  bnj976  31155  bnj66  31237  bnj124  31248  bnj607  31293  bnj873  31301  bnj1234  31388  bnj1463  31430  frrlem1  32086  dssmapf1od  38817  fnchoice  39687  choicefi  39891  axccdom  39915  dfafn5b  41747  cshword2  41947  rngchomffvalALTV  42505
  Copyright terms: Public domain W3C validator