Theorem fneq1 6660

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537  dom cdm 5689  Fun wfun 6557   Fn wfn 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-fun 6565  df-fn 6566

This theorem is referenced by:  fneq1d  6662  fneq1i  6666  fn0  6700  feq1  6717  foeq1  6817  f1ocnv  6861  dffn5  6967  mpteqb  7035  fnsnb  7186  fnprb  7228  fntpb  7229  eufnfv  7249  frrlem1  8310  frrlem13  8322  wfrlem1OLD  8347  wfrlem3OLDa  8350  wfrlem15OLD  8362  tfrlem12  8428  fsetdmprc0  8894  mapval2  8911  elixp2  8940  ixpfn  8942  elixpsn  8976  inf3lem6  9671  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  aceq3lem  10158  dfac4  10160  dfacacn  10180  axcc2lem  10474  axcc3  10476  seqof  14097  ccatvalfn  14616  cshword  14826  0csh0  14828  rrgsupp  20718  lmodfopnelem1  20913  elpt  23596  elptr  23597  ptcmplem3  24078  prdsxmslem2  24558  tgjustr  28497  bnj62  34713  bnj976  34770  bnj66  34853  bnj124  34864  bnj607  34909  bnj873  34917  bnj1234  35006  bnj1463  35048  fineqvac  35090  gblacfnacd  35092  fnsnbt  42250  eqresfnbd  42252  dssmapf1od  44011  fnchoice  44967  choicefi  45143  axccdom  45165  dfafn5b  47111  rngchomffvalALTV  48122  functhinclem1  48841