Theorem fneq1 6623

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 6553	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5887	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2762	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6536	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6536	. 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 5655  Fun wfun 6527   Fn wfn 6528

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-fun 6535  df-fn 6536

This theorem is used by:  fneq1d  6625  fneq1i  6629  fn0  6663  feq1  6680  foeq1  6785  f1ocnv  6830  dffn5  6936  mpteqb  7006  fnsnbg  7162  fnsnbOLD  7164  fnprb  7207  fntpb  7208  eufnfv  7228  frrlem1  8285  frrlem13  8297  tfrlem12  8378  fsetdmprc0  8856  mapval2  8879  elixp2  8908  ixpfn  8910  elixpsn  8944  inf3lem6  9612  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  aceq3lem  10123  dfac4  10125  dfacacn  10144  axcc2lem  10438  axcc3  10440  seqof  14123  ccatvalfn  14646  cshword  14862  0csh0  14864  rrgsupp  20863  lmodfopnelem1  21082  elpt  23798  elptr  23799  ptcmplem3  24280  prdsxmslem2  24755  tgjustr  28815  esplyind  34085  bnj62  35230  bnj976  35287  bnj66  35369  bnj124  35380  bnj607  35425  bnj873  35433  bnj1234  35522  bnj1463  35564  fineqvac  35642  fineqvnttrclse  35650  gblacfnacd  35699  eqresfnbd  43102  dssmapf1od  44861  fnchoice  45863  choicefi  46031  axccdom  46052  dfafn5b  48049  rngchomffvalALTV  49193  ixpv  49816  iinfconstbaslem  49991  iinfconstbas  49992  nelsubc3lem  49996  functhinclem1  50370  cnelsubclem  50529