Theorem fneq1 6555

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 6483	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5825	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2738	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 632	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6461	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6461	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 314	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1539  dom cdm 5600  Fun wfun 6452   Fn wfn 6453

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3306  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-rel 5607  df-cnv 5608  df-co 5609  df-dm 5610  df-fun 6460  df-fn 6461

This theorem is referenced by:  fneq1d  6557  fneq1i  6561  fn0  6594  feq1  6611  foeq1  6714  f1ocnv  6758  dffn5  6860  mpteqb  6926  fnsnb  7070  fnprb  7116  fntpb  7117  eufnfv  7137  frrlem1  8133  frrlem13  8145  wfrlem1OLD  8170  wfrlem3OLDa  8173  wfrlem15OLD  8185  tfrlem12  8251  fsetdmprc0  8674  mapval2  8691  elixp2  8720  ixpfn  8722  elixpsn  8756  inf3lem6  9439  ssttrcl  9521  ttrcltr  9522  ttrclss  9526  ttrclselem2  9532  aceq3lem  9926  dfac4  9928  dfacacn  9947  axcc2lem  10242  axcc3  10244  seqof  13830  ccatvalfn  14335  cshword  14553  0csh0  14555  lmodfopnelem1  20208  rrgsupp  20611  elpt  22772  elptr  22773  ptcmplem3  23254  prdsxmslem2  23734  tgjustr  26884  bnj62  32748  bnj976  32806  bnj66  32889  bnj124  32900  bnj607  32945  bnj873  32953  bnj1234  33042  bnj1463  33084  fineqvac  33115  fnsnbt  40403  dssmapf1od  41842  fnchoice  42785  choicefi  42960  axccdom  42982  dfafn5b  44897  rngchomffvalALTV  45797  functhinclem1  46566