Theorem fneq2i 6644

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

Syntax hints:   ↔ wb 205   = wceq 1541   Fn wfn 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-fn 6543

This theorem is referenced by:  fnunop  6662  fnprb  7206  fntpb  7207  fnsuppeq0  8173  tpos0  8237  wfrlem5OLD  8309  dfixp  8889  ordtypelem4  9512  ser0f  14017  0csh0  14739  s3fn  14858  prodf1f  15834  efcvgfsum  16025  prmrec  16851  fnpr2o  17499  0ssc  17783  0subcat  17784  mulgfvi  18950  ovolunlem1  25005  volsup  25064  mtest  25907  mtestbdd  25908  pserulm  25925  pserdvlem2  25931  emcllem5  26493  lgamgulm2  26529  lgamcvglem  26533  gamcvg2lem  26552  tglnfn  27787  crctcshlem4  29063  fsuppcurry1  31937  fsuppcurry2  31938  resf1o  31942  s2rn  32097  s3rn  32099  cycpmfvlem  32258  cycpmfv3  32261  esumfsup  33056  esumpcvgval  33064  esumcvg  33072  esumsup  33075  bnj149  33874  bnj1312  34057  faclimlem1  34701  fullfunfnv  34906  knoppcnlem8  35364  knoppcnlem11  35367  mblfinlem2  36514  ovoliunnfl  36518  voliunnfl  36520  subsaliuncl  45060  fcores  45763