Theorem fneq1 6580

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 6509	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5849	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2735	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6492	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6492	. 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 5621  Fun wfun 6483   Fn wfn 6484

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-fun 6491  df-fn 6492

This theorem is referenced by:  fneq1d  6582  fneq1i  6586  fn0  6620  feq1  6637  foeq1  6739  f1ocnv  6783  dffn5  6889  mpteqb  6957  fnsnbg  7107  fnsnbOLD  7109  fnprb  7151  fntpb  7152  eufnfv  7172  frrlem1  8225  frrlem13  8237  tfrlem12  8317  fsetdmprc0  8788  mapval2  8806  elixp2  8835  ixpfn  8837  elixpsn  8871  inf3lem6  9534  ssttrcl  9616  ttrcltr  9617  ttrclss  9621  ttrclselem2  9627  aceq3lem  10022  dfac4  10024  dfacacn  10044  axcc2lem  10338  axcc3  10340  seqof  13973  ccatvalfn  14495  cshword  14705  0csh0  14707  rrgsupp  20625  lmodfopnelem1  20840  elpt  23507  elptr  23508  ptcmplem3  23989  prdsxmslem2  24464  tgjustr  28472  esplyind  33659  bnj62  34804  bnj976  34861  bnj66  34944  bnj124  34955  bnj607  35000  bnj873  35008  bnj1234  35097  bnj1463  35139  fineqvac  35211  fineqvnttrclse  35216  gblacfnacd  35218  eqresfnbd  42403  dssmapf1od  44178  fnchoice  45190  choicefi  45360  axccdom  45382  dfafn5b  47323  rngchomffvalALTV  48440  ixpv  49051  iinfconstbaslem  49226  iinfconstbas  49227  nelsubc3lem  49231  functhinclem1  49605  cnelsubclem  49764