Theorem fneq1 6624

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567  dom cdm 5659  Fun wfun 6527   Fn wfn 6528

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6535  df-fn 6536

This theorem is referenced by:  fneq1d  6626  fneq1i  6630  fn0  6664  feq1  6681  foeq1  6786  f1ocnv  6831  dffn5  6937  mpteqb  7007  fnsnbg  7160  fnsnbOLD  7162  fnprb  7204  fntpb  7205  eufnfv  7225  frrlem1  8279  frrlem13  8291  tfrlem12  8372  fsetdmprc0  8848  mapval2  8866  elixp2  8895  ixpfn  8897  elixpsn  8931  inf3lem6  9598  ssttrcl  9680  ttrcltr  9681  ttrclss  9685  ttrclselem2  9691  aceq3lem  10100  dfac4  10102  dfacacn  10121  axcc2lem  10416  axcc3  10418  seqof  14091  ccatvalfn  14614  cshword  14824  0csh0  14826  rrgsupp  20782  lmodfopnelem1  20993  elpt  23694  elptr  23695  ptcmplem3  24176  prdsxmslem2  24651  tgjustr  28705  esplyind  33906  bnj62  35050  bnj976  35107  bnj66  35189  bnj124  35200  bnj607  35245  bnj873  35253  bnj1234  35342  bnj1463  35384  fineqvac  35448  fineqvnttrclse  35456  gblacfnacd  35481  eqresfnbd  42886  dssmapf1od  44632  fnchoice  45634  choicefi  45802  axccdom  45823  dfafn5b  47780  rngchomffvalALTV  48925  ixpv  49546  iinfconstbaslem  49721  iinfconstbas  49722  nelsubc3lem  49726  functhinclem1  50100  cnelsubclem  50259