Theorem fneq1 6446

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 6377	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5774	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2825	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6360	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6360	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 316	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537  dom cdm 5557  Fun wfun 6351   Fn wfn 6352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-fun 6359  df-fn 6360

This theorem is referenced by:  fneq1d  6448  fneq1i  6452  fn0  6481  feq1  6497  foeq1  6588  f1ocnv  6629  dffn5  6726  mpteqb  6789  fnsnb  6930  fnprb  6973  fntpb  6974  eufnfv  6993  wfrlem1  7956  wfrlem3a  7959  wfrlem15  7971  tfrlem12  8027  mapval2  8438  elixp2  8467  ixpfn  8469  elixpsn  8503  inf3lem6  9098  aceq3lem  9548  dfac4  9550  dfacacn  9569  axcc2lem  9860  axcc3  9862  seqof  13430  ccatvalfn  13937  cshword  14155  0csh0  14157  lmodfopnelem1  19672  rrgsupp  20066  elpt  22182  elptr  22183  ptcmplem3  22664  prdsxmslem2  23141  tgjustr  26262  bnj62  31992  bnj976  32051  bnj66  32134  bnj124  32145  bnj607  32190  bnj873  32198  bnj1234  32287  bnj1463  32329  frrlem1  33125  frrlem13  33137  fnsnbt  39127  dssmapf1od  40374  fnchoice  41293  choicefi  41470  axccdom  41494  dfafn5b  43367  rngchomffvalALTV  44273