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 6587	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5897	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2765	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6569	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6569	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  dom cdm 5658  Fun wfun 6560   Fn wfn 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-fun 6568  df-fn 6569

This theorem is used by:  fneq1d  6662  fneq1i  6666  fn0  6700  feq1  6717  foeq1  6822  f1ocnv  6867  dffn5  6974  mpteqb  7044  fnsnbg  7201  fnprb  7245  fntpb  7246  eufnfv  7266  frrlem1  8342  frrlem13  8354  tfrlem12  8435  fsetdmprc0  8915  mapval2  8938  elixp2  8967  ixpfn  8969  elixpsn  9003  inf3lem6  9671  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  aceq3lem  10238  dfac4  10240  dfacacn  10259  axcc2lem  10553  axcc3  10555  seqof  14242  ccatvalfn  14767  cshword  14984  0csh0  14986  rrgsupp  21004  lmodfopnelem1  21224  elpt  23946  elptr  23947  ptcmplem3  24428  prdsxmslem2  24903  tgjustr  28993  esplyind  34318  bnj62  35462  bnj976  35519  bnj66  35601  bnj124  35612  bnj607  35657  bnj873  35665  bnj1234  35754  bnj1463  35796  fineqvac  35925  fineqvnttrclse  35933  gblacfnacd  36070  mirimanoffr  36668  nvof1ob  38231  eqresfnbd  43553  dssmapf1od  45282  fnchoice  46320  choicefi  46487  axccdom  46508  dfafn5b  48504  rngchomffvalALTV  49648  ixpv  50334  iinfconstbaslem  50510  iinfconstbas  50511  nelsubc3lem  50515  functhinclem1  50910  cnelsubcw  51072