Theorem fneq2i 6677

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

Syntax hints:   ↔ wb 206   = wceq 1537   Fn wfn 6568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576

This theorem is referenced by:  fnunop  6695  fnprb  7245  fntpb  7246  fnsuppeq0  8233  tpos0  8297  wfrlem5OLD  8369  dfixp  8957  ordtypelem4  9590  ser0f  14106  0csh0  14841  s3fn  14960  prodf1f  15940  efcvgfsum  16134  prmrec  16969  fnpr2o  17617  0ssc  17901  0subcat  17902  mulgfvi  19113  ovolunlem1  25551  volsup  25610  mtest  26465  mtestbdd  26466  pserulm  26483  pserdvlem2  26490  emcllem5  27061  lgamgulm2  27097  lgamcvglem  27101  gamcvg2lem  27120  tglnfn  28573  crctcshlem4  29853  fsuppcurry1  32739  fsuppcurry2  32740  resf1o  32744  s2rnOLD  32910  s3rnOLD  32912  cycpmfvlem  33105  cycpmfv3  33108  esumfsup  34034  esumpcvgval  34042  esumcvg  34050  esumsup  34053  bnj149  34851  bnj1312  35034  faclimlem1  35705  fullfunfnv  35910  ixpeq1i  36164  cbvixpvw2  36211  knoppcnlem8  36466  knoppcnlem11  36469  mblfinlem2  37618  ovoliunnfl  37622  voliunnfl  37624  subsaliuncl  46279  fcores  46982