Theorem fneq1 6520

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 6450	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5809	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2741	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 630	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6433	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6433	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 313	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1541  dom cdm 5588  Fun wfun 6424   Fn wfn 6425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-fun 6432  df-fn 6433

This theorem is referenced by:  fneq1d  6522  fneq1i  6526  fn0  6560  feq1  6577  foeq1  6680  f1ocnv  6724  dffn5  6822  mpteqb  6888  fnsnb  7032  fnprb  7078  fntpb  7079  eufnfv  7099  frrlem1  8086  frrlem13  8098  wfrlem1OLD  8123  wfrlem3OLDa  8126  wfrlem15OLD  8138  tfrlem12  8204  fsetdmprc0  8617  mapval2  8634  elixp2  8663  ixpfn  8665  elixpsn  8699  inf3lem6  9352  ssttrcl  9434  ttrcltr  9435  ttrclss  9439  ttrclselem2  9445  aceq3lem  9860  dfac4  9862  dfacacn  9881  axcc2lem  10176  axcc3  10178  seqof  13761  ccatvalfn  14267  cshword  14485  0csh0  14487  lmodfopnelem1  20140  rrgsupp  20543  elpt  22704  elptr  22705  ptcmplem3  23186  prdsxmslem2  23666  tgjustr  26816  bnj62  32678  bnj976  32736  bnj66  32819  bnj124  32830  bnj607  32875  bnj873  32883  bnj1234  32972  bnj1463  33014  fineqvac  33045  fnsnbt  40188  dssmapf1od  41582  fnchoice  42525  choicefi  42693  axccdom  42715  dfafn5b  44604  rngchomffvalALTV  45505  functhinclem1  46274