Theorem fneq1 6630

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 6560	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5895	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2767	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6543	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6543	. 2 ⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴))
7	4, 5, 6	3bitr4g 317	1 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570  dom cdm 5663  Fun wfun 6534   Fn wfn 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6542  df-fn 6543

This theorem is used by:  fneq1d  6632  fneq1i  6636  fn0  6670  feq1  6687  foeq1  6792  f1ocnv  6837  dffn5  6943  mpteqb  7013  fnsnbg  7166  fnsnbOLD  7168  fnprb  7210  fntpb  7211  eufnfv  7231  frrlem1  8285  frrlem13  8297  tfrlem12  8378  fsetdmprc0  8854  mapval2  8872  elixp2  8901  ixpfn  8903  elixpsn  8937  inf3lem6  9605  ssttrcl  9687  ttrcltr  9688  ttrclss  9692  ttrclselem2  9698  aceq3lem  10116  dfac4  10118  dfacacn  10137  axcc2lem  10431  axcc3  10433  seqof  14108  ccatvalfn  14631  cshword  14847  0csh0  14849  rrgsupp  20829  lmodfopnelem1  21048  elpt  23758  elptr  23759  ptcmplem3  24240  prdsxmslem2  24715  tgjustr  28772  esplyind  33988  bnj62  35133  bnj976  35190  bnj66  35272  bnj124  35283  bnj607  35328  bnj873  35336  bnj1234  35425  bnj1463  35467  fineqvac  35545  fineqvnttrclse  35553  gblacfnacd  35602  eqresfnbd  43036  dssmapf1od  44780  fnchoice  45782  choicefi  45950  axccdom  45971  dfafn5b  47931  rngchomffvalALTV  49076  ixpv  49701  iinfconstbaslem  49876  iinfconstbas  49877  nelsubc3lem  49881  functhinclem1  50255  cnelsubclem  50414