Theorem fneq1 5937

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 5867	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5284	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2623	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 746	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 5850	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 5850	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 303	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480  dom cdm 5074  Fun wfun 5841   Fn wfn 5842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-fun 5849  df-fn 5850

This theorem is referenced by:  fneq1d  5939  fneq1i  5943  fn0  5968  feq1  5983  foeq1  6068  f1ocnv  6106  dffn5  6198  mpteqb  6255  fnsnb  6386  fnprb  6426  fntpb  6427  eufnfv  6445  wfrlem1  7359  wfrlem3a  7362  wfrlem15  7374  tfrlem12  7430  mapval2  7831  elixp2  7856  ixpfn  7858  elixpsn  7891  inf3lem6  8474  aceq3lem  8887  dfac4  8889  dfacacn  8907  axcc2lem  9202  axcc3  9204  seqof  12798  ccatvalfn  13304  cshword  13474  0csh0  13476  lmodfopnelem1  18820  rrgsupp  19210  elpt  21285  elptr  21286  ptcmplem3  21768  prdsxmslem2  22244  bnj62  30491  bnj976  30553  bnj66  30635  bnj124  30646  bnj607  30691  bnj873  30699  bnj1234  30786  bnj1463  30828  frrlem1  31478  dssmapf1od  37794  fnchoice  38668  choicefi  38863  axccdom  38887  dfafn5b  40542  cshword2  40733  rngchomffvalALTV  41280