Theorem fneq2i 6647

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

Syntax hints:   ↔ wb 205   = wceq 1540   Fn wfn 6538

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

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

This theorem is referenced by:  fnunop  6665  fnprb  7212  fntpb  7213  fnsuppeq0  8182  tpos0  8247  wfrlem5OLD  8319  dfixp  8899  ordtypelem4  9522  ser0f  14028  0csh0  14750  s3fn  14869  prodf1f  15845  efcvgfsum  16036  prmrec  16862  fnpr2o  17510  0ssc  17794  0subcat  17795  mulgfvi  18999  ovolunlem1  25346  volsup  25405  mtest  26255  mtestbdd  26256  pserulm  26273  pserdvlem2  26280  emcllem5  26845  lgamgulm2  26881  lgamcvglem  26885  gamcvg2lem  26904  tglnfn  28231  crctcshlem4  29507  fsuppcurry1  32383  fsuppcurry2  32384  resf1o  32388  s2rn  32543  s3rn  32545  cycpmfvlem  32707  cycpmfv3  32710  esumfsup  33532  esumpcvgval  33540  esumcvg  33548  esumsup  33551  bnj149  34350  bnj1312  34533  faclimlem1  35183  fullfunfnv  35388  knoppcnlem8  35840  knoppcnlem11  35843  mblfinlem2  36990  ovoliunnfl  36994  voliunnfl  36996  subsaliuncl  45533  fcores  46236