Theorem fneq1 6277

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 6208	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5622	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2780	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 621	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6191	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6191	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 306	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   = wceq 1507  dom cdm 5407  Fun wfun 6182   Fn wfn 6183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-fun 6190  df-fn 6191

This theorem is referenced by:  fneq1d  6279  fneq1i  6283  fn0  6309  feq1  6325  foeq1  6415  f1ocnv  6456  dffn5  6554  mpteqb  6613  fnsnb  6751  fnprb  6797  fntpb  6798  eufnfv  6817  wfrlem1  7757  wfrlem3a  7760  wfrlem15  7773  tfrlem12  7829  mapval2  8236  elixp2  8263  ixpfn  8265  elixpsn  8298  inf3lem6  8890  aceq3lem  9340  dfac4  9342  dfacacn  9361  axcc2lem  9656  axcc3  9658  seqof  13242  ccatvalfn  13744  cshword  14013  0csh0  14016  0csh0OLD  14017  lmodfopnelem1  19392  rrgsupp  19785  elpt  21884  elptr  21885  ptcmplem3  22366  prdsxmslem2  22842  tgjustr  25962  bnj62  31644  bnj976  31703  bnj66  31785  bnj124  31796  bnj607  31841  bnj873  31849  bnj1234  31936  bnj1463  31978  frrlem1  32650  frrlem13  32662  fnsnbt  38571  dssmapf1od  39736  fnchoice  40711  choicefi  40894  axccdom  40918  dfafn5b  42772  rngchomffvalALTV  43636