Theorem fneq1 6628

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  dom cdm 5663  Fun wfun 6532   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6540  df-fn 6541

This theorem is referenced by:  fneq1d  6630  fneq1i  6634  fn0  6668  feq1  6685  foeq1  6790  f1ocnv  6835  dffn5  6941  mpteqb  7011  fnsnbg  7164  fnsnbOLD  7166  fnprb  7208  fntpb  7209  eufnfv  7229  frrlem1  8284  frrlem13  8296  tfrlem12  8377  fsetdmprc0  8853  mapval2  8871  elixp2  8900  ixpfn  8902  elixpsn  8936  inf3lem6  9603  ssttrcl  9685  ttrcltr  9686  ttrclss  9690  ttrclselem2  9696  aceq3lem  10105  dfac4  10107  dfacacn  10126  axcc2lem  10421  axcc3  10423  seqof  14097  ccatvalfn  14620  cshword  14830  0csh0  14832  rrgsupp  20787  lmodfopnelem1  21000  elpt  23710  elptr  23711  ptcmplem3  24192  prdsxmslem2  24667  tgjustr  28724  esplyind  33946  bnj62  35090  bnj976  35147  bnj66  35229  bnj124  35240  bnj607  35285  bnj873  35293  bnj1234  35382  bnj1463  35424  fineqvac  35510  fineqvnttrclse  35518  gblacfnacd  35567  eqresfnbd  42984  dssmapf1od  44730  fnchoice  45732  choicefi  45900  axccdom  45921  dfafn5b  47881  rngchomffvalALTV  49026  ixpv  49651  iinfconstbaslem  49826  iinfconstbas  49827  nelsubc3lem  49831  functhinclem1  50205  cnelsubclem  50364