Theorem fneq1 6583

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 6512	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5852	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2738	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6495	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6495	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  dom cdm 5624  Fun wfun 6486   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  fneq1d  6585  fneq1i  6589  fn0  6623  feq1  6640  foeq1  6742  f1ocnv  6786  dffn5  6892  mpteqb  6960  fnsnbg  7110  fnsnbOLD  7112  fnprb  7154  fntpb  7155  eufnfv  7175  frrlem1  8228  frrlem13  8240  tfrlem12  8320  fsetdmprc0  8792  mapval2  8810  elixp2  8839  ixpfn  8841  elixpsn  8875  inf3lem6  9542  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  aceq3lem  10030  dfac4  10032  dfacacn  10052  axcc2lem  10346  axcc3  10348  seqof  13982  ccatvalfn  14504  cshword  14714  0csh0  14716  rrgsupp  20634  lmodfopnelem1  20849  elpt  23516  elptr  23517  ptcmplem3  23998  prdsxmslem2  24473  tgjustr  28546  esplyind  33731  bnj62  34876  bnj976  34933  bnj66  35016  bnj124  35027  bnj607  35072  bnj873  35080  bnj1234  35169  bnj1463  35211  fineqvac  35272  fineqvnttrclse  35280  gblacfnacd  35296  eqresfnbd  42488  dssmapf1od  44262  fnchoice  45274  choicefi  45444  axccdom  45466  dfafn5b  47407  rngchomffvalALTV  48524  ixpv  49135  iinfconstbaslem  49310  iinfconstbas  49311  nelsubc3lem  49315  functhinclem1  49689  cnelsubclem  49848