Theorem fneq1 6589

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 6518	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5858	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2738	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 633	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6501	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6501	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542  dom cdm 5631  Fun wfun 6492   Fn wfn 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6500  df-fn 6501

This theorem is referenced by:  fneq1d  6591  fneq1i  6595  fn0  6629  feq1  6646  foeq1  6748  f1ocnv  6792  dffn5  6898  mpteqb  6967  fnsnbg  7119  fnsnbOLD  7121  fnprb  7163  fntpb  7164  eufnfv  7184  frrlem1  8236  frrlem13  8248  tfrlem12  8328  fsetdmprc0  8802  mapval2  8820  elixp2  8849  ixpfn  8851  elixpsn  8885  inf3lem6  9554  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  aceq3lem  10042  dfac4  10044  dfacacn  10064  axcc2lem  10358  axcc3  10360  seqof  14021  ccatvalfn  14543  cshword  14753  0csh0  14755  rrgsupp  20678  lmodfopnelem1  20893  elpt  23537  elptr  23538  ptcmplem3  24019  prdsxmslem2  24494  tgjustr  28542  esplyind  33719  bnj62  34863  bnj976  34920  bnj66  35002  bnj124  35013  bnj607  35058  bnj873  35066  bnj1234  35155  bnj1463  35197  fineqvac  35260  fineqvnttrclse  35268  gblacfnacd  35284  eqresfnbd  42673  dssmapf1od  44448  fnchoice  45460  choicefi  45629  axccdom  45651  dfafn5b  47609  rngchomffvalALTV  48754  ixpv  49365  iinfconstbaslem  49540  iinfconstbas  49541  nelsubc3lem  49545  functhinclem1  49919  cnelsubclem  50078