Theorem fneq2i 6580

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

Syntax hints:   ↔ wb 206   = wceq 1540   Fn wfn 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6485

This theorem is referenced by:  fnunop  6598  fnprb  7144  fntpb  7145  fnsuppeq0  8125  tpos0  8189  dfixp  8826  ordtypelem4  9413  ser0f  13962  0csh0  14699  s3fn  14818  prodf1f  15799  efcvgfsum  15993  prmrec  16834  fnpr2o  17461  0ssc  17744  0subcat  17745  mulgfvi  18952  ovolunlem1  25396  volsup  25455  mtest  26311  mtestbdd  26312  pserulm  26329  pserdvlem2  26336  emcllem5  26908  lgamgulm2  26944  lgamcvglem  26948  gamcvg2lem  26967  tglnfn  28492  crctcshlem4  29765  fsuppcurry1  32668  fsuppcurry2  32669  resf1o  32673  s2rnOLD  32885  s3rnOLD  32887  cycpmfvlem  33054  cycpmfv3  33057  esumfsup  34037  esumpcvgval  34045  esumcvg  34053  esumsup  34056  bnj149  34842  bnj1312  35025  faclimlem1  35716  fullfunfnv  35920  ixpeq1i  36174  cbvixpvw2  36219  knoppcnlem8  36474  knoppcnlem11  36477  mblfinlem2  37638  ovoliunnfl  37642  voliunnfl  37644  subsaliuncl  46339  fcores  47051  isubgr3stgrlem7  47956  isofval2  49017  0funcALT  49073