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

Theorem fneq1 5947
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 5877 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2 dmeq 5294 . . . 4 (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
32eqeq1d 2623 . . 3 (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
41, 3anbi12d 746 . 2 (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5 df-fn 5860 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6 df-fn 5860 . 2 (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
74, 5, 63bitr4g 303 1 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  dom cdm 5084  Fun wfun 5851   Fn wfn 5852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-br 4624  df-opab 4684  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-fun 5859  df-fn 5860
This theorem is referenced by:  fneq1d  5949  fneq1i  5953  fn0  5978  feq1  5993  foeq1  6078  f1ocnv  6116  dffn5  6208  mpteqb  6265  fnsnb  6397  fnprb  6437  fntpb  6438  eufnfv  6456  wfrlem1  7374  wfrlem3a  7377  wfrlem15  7389  tfrlem12  7445  mapval2  7847  elixp2  7872  ixpfn  7874  elixpsn  7907  inf3lem6  8490  aceq3lem  8903  dfac4  8905  dfacacn  8923  axcc2lem  9218  axcc3  9220  seqof  12814  ccatvalfn  13320  cshword  13490  0csh0  13492  lmodfopnelem1  18839  rrgsupp  19231  elpt  21315  elptr  21316  ptcmplem3  21798  prdsxmslem2  22274  bnj62  30547  bnj976  30609  bnj66  30691  bnj124  30702  bnj607  30747  bnj873  30755  bnj1234  30842  bnj1463  30884  frrlem1  31534  dssmapf1od  37836  fnchoice  38710  choicefi  38901  axccdom  38925  dfafn5b  40575  cshword2  40766  rngchomffvalALTV  41313
  Copyright terms: Public domain W3C validator