Theorem fneq1 6628

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 6557	. . 3 ⊢ (𝐹 = 𝐺 → (Fun 𝐹 ↔ Fun 𝐺))
2		dmeq 5885	. . . 4 ⊢ (𝐹 = 𝐺 → dom 𝐹 = dom 𝐺)
3	2	eqeq1d 2763	. . 3 ⊢ (𝐹 = 𝐺 → (dom 𝐹 = 𝐴 ↔ dom 𝐺 = 𝐴))
4	1, 3	anbi12d 644	. 2 ⊢ (𝐹 = 𝐺 → ((Fun 𝐹 ∧ dom 𝐹 = 𝐴) ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)))
5		df-fn 6540	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
6		df-fn 6540	. 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 5651  Fun wfun 6531   Fn wfn 6532

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6539  df-fn 6540

This theorem is used by:  fneq1d  6630  fneq1i  6634  fn0  6668  feq1  6685  foeq1  6790  f1ocnv  6835  dffn5  6941  mpteqb  7011  fnsnbg  7167  fnsnbOLD  7169  fnprb  7212  fntpb  7213  eufnfv  7233  frrlem1  8297  frrlem13  8309  tfrlem12  8390  fsetdmprc0  8870  mapval2  8893  elixp2  8922  ixpfn  8924  elixpsn  8958  inf3lem6  9627  ssttrcl  9709  ttrcltr  9710  ttrclss  9714  ttrclselem2  9720  aceq3lem  10192  dfac4  10194  dfacacn  10213  axcc2lem  10507  axcc3  10509  seqof  14195  ccatvalfn  14719  cshword  14935  0csh0  14937  rrgsupp  20946  lmodfopnelem1  21166  elpt  23884  elptr  23885  ptcmplem3  24366  prdsxmslem2  24841  tgjustr  28929  esplyind  34200  bnj62  35344  bnj976  35401  bnj66  35483  bnj124  35494  bnj607  35539  bnj873  35547  bnj1234  35636  bnj1463  35678  fineqvac  35767  fineqvnttrclse  35775  gblacfnacd  35864  eqresfnbd  43266  dssmapf1od  45006  fnchoice  46015  choicefi  46183  axccdom  46204  dfafn5b  48200  rngchomffvalALTV  49344  ixpv  49967  iinfconstbaslem  50142  iinfconstbas  50143  nelsubc3lem  50147  functhinclem1  50521  cnelsubclem  50680