Theorem fneq1 6448

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 6378	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5757	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2738	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 634	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6361	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6361	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1543  dom cdm 5536  Fun wfun 6352   Fn wfn 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040  df-opab 5102  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-fun 6360  df-fn 6361

This theorem is referenced by:  fneq1d  6450  fneq1i  6454  fn0  6487  feq1  6504  foeq1  6607  f1ocnv  6651  dffn5  6749  mpteqb  6815  fnsnb  6959  fnprb  7002  fntpb  7003  eufnfv  7023  frrlem1  8005  frrlem13  8017  wfrlem1  8032  wfrlem3a  8035  wfrlem15  8047  tfrlem12  8103  fsetdmprc0  8514  mapval2  8531  elixp2  8560  ixpfn  8562  elixpsn  8596  inf3lem6  9226  aceq3lem  9699  dfac4  9701  dfacacn  9720  axcc2lem  10015  axcc3  10017  seqof  13598  ccatvalfn  14103  cshword  14321  0csh0  14323  lmodfopnelem1  19889  rrgsupp  20283  elpt  22423  elptr  22424  ptcmplem3  22905  prdsxmslem2  23381  tgjustr  26519  bnj62  32365  bnj976  32424  bnj66  32507  bnj124  32518  bnj607  32563  bnj873  32571  bnj1234  32660  bnj1463  32702  fineqvac  32733  fnsnbt  39862  dssmapf1od  41247  fnchoice  42186  choicefi  42354  axccdom  42376  dfafn5b  44268  rngchomffvalALTV  45169  functhinclem1  45938