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

Theorem fneq1 6184
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 6115 . . 3 (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2 dmeq 5519 . . . 4 (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
32eqeq1d 2804 . . 3 (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
41, 3anbi12d 618 . 2 (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5 df-fn 6098 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6 df-fn 6098 . 2 (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
74, 5, 63bitr4g 305 1 (𝐹 = 𝐺 → (𝐹 Fn 𝐴𝐺 Fn 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  dom cdm 5305  Fun wfun 6089   Fn wfn 6090
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-rab 3101  df-v 3389  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-nul 4111  df-if 4274  df-sn 4365  df-pr 4367  df-op 4371  df-br 4838  df-opab 4900  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-fun 6097  df-fn 6098
This theorem is referenced by:  fneq1d  6186  fneq1i  6190  fn0  6216  feq1  6231  foeq1  6321  f1ocnv  6359  dffn5  6456  mpteqb  6514  fnsnb  6651  fnprb  6691  fntpb  6692  eufnfv  6710  wfrlem1  7643  wfrlem3a  7646  wfrlem15  7659  tfrlem12  7715  mapval2  8116  elixp2  8143  ixpfn  8145  elixpsn  8178  inf3lem6  8771  aceq3lem  9220  dfac4  9222  dfacacn  9242  axcc2lem  9537  axcc3  9539  seqof  13075  ccatvalfn  13572  cshword  13755  0csh0  13757  lmodfopnelem1  19097  rrgsupp  19494  elpt  21583  elptr  21584  ptcmplem3  22065  prdsxmslem2  22541  bnj62  31105  bnj976  31165  bnj66  31247  bnj124  31258  bnj607  31303  bnj873  31311  bnj1234  31398  bnj1463  31440  frrlem1  32095  dssmapf1od  38809  fnchoice  39676  choicefi  39873  axccdom  39897  dfafn5b  41744  cshword2  42006  rngchomffvalALTV  42557
  Copyright terms: Public domain W3C validator