Theorem fneq2i 6640

Description: Equality inference for function predicate with domain. (Contributed by NM, 4-Sep-2011.)

Hypothesis

Ref	Expression
fneq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
fneq2i	⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)

Proof of Theorem fneq2i

Step	Hyp	Ref	Expression
1		fneq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		fneq2 6634	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   Fn wfn 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6544

This theorem is used by:  fnunop  6658  fnprb  7216  fntpb  7217  fnsuppeq0  8214  tpos0  8278  dfixp  8932  ordtypelem4  9520  imadomnum  10619  ser0f  14203  0csh0  14950  s3fn  15069  prodf1f  16068  efcvgfsum  16259  prmrec  17107  fnpr2o  17736  0ssc  18019  0subcat  18020  mulgfvi  19290  ovolunlem1  25825  volsup  25884  mtest  26738  mtestbdd  26739  pserulm  26756  pserdvlem2  26762  emcllem5  27334  lgamgulm2  27370  lgamcvglem  27374  gamcvg2lem  27393  tglnfn  29017  tgplnfn  29260  crctcshlem4  30416  fsuppcurry1  33364  fsuppcurry2  33365  resf1o  33370  cycpmfvlem  33721  cycpmfv3  33724  selvply1rhmlemb  34199  esumfsup  34750  esumpcvgval  34758  esumcvg  34766  esumsup  34769  bnj149  35553  bnj1312  35736  faclimlem1  36602  fullfunfnv  36804  ixpeq1i  37083  cbvixpvw2  37128  knoppcnlem8  37460  knoppcnlem11  37463  mblfinlem2  38683  ovoliunnfl  38687  voliunnfl  38689  subsaliuncl  47475  fcores  48244  isubgr3stgrlem7  49177  isofval2  50253  0funcALT  50310