Theorem fneq2i 6574

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 6568	. 2 ⊢ (𝐴 = 𝐵 → (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐵)

Syntax hints:   ↔ wb 206   = wceq 1541   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-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6479

This theorem is referenced by:  fnunop  6592  fnprb  7137  fntpb  7138  fnsuppeq0  8117  tpos0  8181  dfixp  8818  ordtypelem4  9402  ser0f  13957  0csh0  14695  s3fn  14813  prodf1f  15794  efcvgfsum  15988  prmrec  16829  fnpr2o  17456  0ssc  17739  0subcat  17740  mulgfvi  18981  ovolunlem1  25420  volsup  25479  mtest  26335  mtestbdd  26336  pserulm  26353  pserdvlem2  26360  emcllem5  26932  lgamgulm2  26968  lgamcvglem  26972  gamcvg2lem  26991  tglnfn  28520  crctcshlem4  29793  fsuppcurry1  32699  fsuppcurry2  32700  resf1o  32705  s2rnOLD  32917  s3rnOLD  32919  cycpmfvlem  33073  cycpmfv3  33076  esumfsup  34075  esumpcvgval  34083  esumcvg  34091  esumsup  34094  bnj149  34879  bnj1312  35062  faclimlem1  35779  fullfunfnv  35980  ixpeq1i  36234  cbvixpvw2  36279  knoppcnlem8  36534  knoppcnlem11  36537  mblfinlem2  37698  ovoliunnfl  37702  voliunnfl  37704  subsaliuncl  46396  fcores  47098  isubgr3stgrlem7  48003  isofval2  49064  0funcALT  49120