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

Theorem fneq1 6418
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 6348 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2 dmeq 5740 . . . 4 (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
32eqeq1d 2803 . . 3 (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
41, 3anbi12d 633 . 2 (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5 df-fn 6331 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6 df-fn 6331 . 2 (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
74, 5, 63bitr4g 317 1 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  dom cdm 5523  Fun wfun 6322   Fn wfn 6323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-fun 6330  df-fn 6331
This theorem is referenced by:  fneq1d  6420  fneq1i  6424  fn0  6455  feq1  6472  foeq1  6565  f1ocnv  6606  dffn5  6703  mpteqb  6768  fnsnb  6909  fnprb  6952  fntpb  6953  eufnfv  6973  wfrlem1  7941  wfrlem3a  7944  wfrlem15  7956  tfrlem12  8012  mapval2  8423  elixp2  8452  ixpfn  8454  elixpsn  8488  inf3lem6  9084  aceq3lem  9535  dfac4  9537  dfacacn  9556  axcc2lem  9851  axcc3  9853  seqof  13427  ccatvalfn  13930  cshword  14148  0csh0  14150  lmodfopnelem1  19666  rrgsupp  20060  elpt  22180  elptr  22181  ptcmplem3  22662  prdsxmslem2  23139  tgjustr  26271  bnj62  32098  bnj976  32157  bnj66  32240  bnj124  32251  bnj607  32296  bnj873  32304  bnj1234  32393  bnj1463  32435  frrlem1  33231  frrlem13  33243  fnsnbt  39401  dssmapf1od  40709  fnchoice  41645  choicefi  41816  axccdom  41840  dfafn5b  43704  rngchomffvalALTV  44606
  Copyright terms: Public domain W3C validator