Theorem fneq1 6567

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541  dom cdm 5611  Fun wfun 6470   Fn wfn 6471

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-fun 6478  df-fn 6479

This theorem is referenced by:  fneq1d  6569  fneq1i  6573  fn0  6607  feq1  6624  foeq1  6726  f1ocnv  6770  dffn5  6875  mpteqb  6943  fnsnbg  7093  fnsnbOLD  7095  fnprb  7137  fntpb  7138  eufnfv  7158  frrlem1  8211  frrlem13  8223  tfrlem12  8303  fsetdmprc0  8774  mapval2  8791  elixp2  8820  ixpfn  8822  elixpsn  8856  inf3lem6  9518  ssttrcl  9600  ttrcltr  9601  ttrclss  9605  ttrclselem2  9611  aceq3lem  10006  dfac4  10008  dfacacn  10028  axcc2lem  10322  axcc3  10324  seqof  13961  ccatvalfn  14483  cshword  14693  0csh0  14695  rrgsupp  20611  lmodfopnelem1  20826  elpt  23482  elptr  23483  ptcmplem3  23964  prdsxmslem2  24439  tgjustr  28447  bnj62  34724  bnj976  34781  bnj66  34864  bnj124  34875  bnj607  34920  bnj873  34928  bnj1234  35017  bnj1463  35059  fineqvac  35131  fineqvnttrclse  35136  gblacfnacd  35138  eqresfnbd  42265  dssmapf1od  44054  fnchoice  45066  choicefi  45237  axccdom  45259  dfafn5b  47192  rngchomffvalALTV  48309  ixpv  48921  iinfconstbaslem  49097  iinfconstbas  49098  nelsubc3lem  49102  functhinclem1  49476  cnelsubclem  49635