Theorem fneq1 6577

Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fneq1	⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Proof of Theorem fneq1

Step	Hyp	Ref	Expression
1		funeq 6506	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5850	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2731	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6489	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6489	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540  dom cdm 5623  Fun wfun 6480   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-fun 6488  df-fn 6489

This theorem is referenced by:  fneq1d  6579  fneq1i  6583  fn0  6617  feq1  6634  foeq1  6736  f1ocnv  6780  dffn5  6885  mpteqb  6953  fnsnbg  7104  fnsnbOLD  7106  fnprb  7148  fntpb  7149  eufnfv  7169  frrlem1  8226  frrlem13  8238  tfrlem12  8318  fsetdmprc0  8789  mapval2  8806  elixp2  8835  ixpfn  8837  elixpsn  8871  inf3lem6  9548  ssttrcl  9630  ttrcltr  9631  ttrclss  9635  ttrclselem2  9641  aceq3lem  10033  dfac4  10035  dfacacn  10055  axcc2lem  10349  axcc3  10351  seqof  13984  ccatvalfn  14506  cshword  14715  0csh0  14717  rrgsupp  20604  lmodfopnelem1  20819  elpt  23475  elptr  23476  ptcmplem3  23957  prdsxmslem2  24433  tgjustr  28437  bnj62  34689  bnj976  34746  bnj66  34829  bnj124  34840  bnj607  34885  bnj873  34893  bnj1234  34982  bnj1463  35024  fineqvac  35074  gblacfnacd  35077  eqresfnbd  42208  dssmapf1od  43997  fnchoice  45010  choicefi  45181  axccdom  45203  dfafn5b  47149  rngchomffvalALTV  48266  ixpv  48878  iinfconstbaslem  49054  iinfconstbas  49055  nelsubc3lem  49059  functhinclem1  49433  cnelsubclem  49592