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  13985  ccatvalfn  14507  cshword  14716  0csh0  14718  rrgsupp  20605  lmodfopnelem1  20820  elpt  23476  elptr  23477  ptcmplem3  23958  prdsxmslem2  24434  tgjustr  28438  bnj62  34706  bnj976  34763  bnj66  34846  bnj124  34857  bnj607  34902  bnj873  34910  bnj1234  34999  bnj1463  35041  fineqvac  35091  gblacfnacd  35094  eqresfnbd  42225  dssmapf1od  44014  fnchoice  45027  choicefi  45198  axccdom  45220  dfafn5b  47165  rngchomffvalALTV  48282  ixpv  48894  iinfconstbaslem  49070  iinfconstbas  49071  nelsubc3lem  49075  functhinclem1  49449  cnelsubclem  49608