Theorem fneq2i 6587

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

Syntax hints:   ↔ wb 206   = wceq 1541   Fn wfn 6484

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 2123  ax-ext 2705

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

This theorem is referenced by:  fnunop  6605  fnprb  7151  fntpb  7152  fnsuppeq0  8131  tpos0  8195  dfixp  8833  ordtypelem4  9418  ser0f  13969  0csh0  14707  s3fn  14825  prodf1f  15806  efcvgfsum  16000  prmrec  16841  fnpr2o  17469  0ssc  17752  0subcat  17753  mulgfvi  18994  ovolunlem1  25445  volsup  25504  mtest  26360  mtestbdd  26361  pserulm  26378  pserdvlem2  26385  emcllem5  26957  lgamgulm2  26993  lgamcvglem  26997  gamcvg2lem  27016  tglnfn  28545  crctcshlem4  29819  fsuppcurry1  32731  fsuppcurry2  32732  resf1o  32737  s2rnOLD  32954  s3rnOLD  32956  cycpmfvlem  33122  cycpmfv3  33125  esumfsup  34155  esumpcvgval  34163  esumcvg  34171  esumsup  34174  bnj149  34959  bnj1312  35142  faclimlem1  35859  fullfunfnv  36062  ixpeq1i  36316  cbvixpvw2  36361  knoppcnlem8  36616  knoppcnlem11  36619  mblfinlem2  37771  ovoliunnfl  37775  voliunnfl  37777  subsaliuncl  46518  fcores  47229  isubgr3stgrlem7  48134  isofval2  49193  0funcALT  49249