Theorem fneq1 6641

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542  dom cdm 5677  Fun wfun 6538   Fn wfn 6539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-fun 6546  df-fn 6547

This theorem is referenced by:  fneq1d  6643  fneq1i  6647  fn0  6682  feq1  6699  foeq1  6802  f1ocnv  6846  dffn5  6951  mpteqb  7018  fnsnb  7164  fnprb  7210  fntpb  7211  eufnfv  7231  frrlem1  8271  frrlem13  8283  wfrlem1OLD  8308  wfrlem3OLDa  8311  wfrlem15OLD  8323  tfrlem12  8389  fsetdmprc0  8849  mapval2  8866  elixp2  8895  ixpfn  8897  elixpsn  8931  inf3lem6  9628  ssttrcl  9710  ttrcltr  9711  ttrclss  9715  ttrclselem2  9721  aceq3lem  10115  dfac4  10117  dfacacn  10136  axcc2lem  10431  axcc3  10433  seqof  14025  ccatvalfn  14531  cshword  14741  0csh0  14743  lmodfopnelem1  20508  rrgsupp  20907  elpt  23076  elptr  23077  ptcmplem3  23558  prdsxmslem2  24038  tgjustr  27725  bnj62  33731  bnj976  33788  bnj66  33871  bnj124  33882  bnj607  33927  bnj873  33935  bnj1234  34024  bnj1463  34066  fineqvac  34097  fnsnbt  41051  eqresfnbd  41054  dssmapf1od  42772  fnchoice  43713  choicefi  43899  axccdom  43921  dfafn5b  45869  rngchomffvalALTV  46893  functhinclem1  47661