Theorem fneq2i 6583

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

Syntax hints:   ↔ wb 207   = wceq 1547   Fn wfn 6480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-fn 6488

This theorem is referenced by:  fnunop  6601  fnprb  7152  fntpb  7153  fnsuppeq0  8132  tpos0  8196  dfixp  8837  ordtypelem4  9426  ser0f  14008  0csh0  14746  s3fn  14864  prodf1f  15848  efcvgfsum  16042  prmrec  16884  fnpr2o  17512  0ssc  17795  0subcat  17796  mulgfvi  19040  ovolunlem1  25482  volsup  25541  mtest  26387  mtestbdd  26388  pserulm  26405  pserdvlem2  26411  emcllem5  26981  lgamgulm2  27017  lgamcvglem  27021  gamcvg2lem  27040  tglnfn  28633  crctcshlem4  29906  fsuppcurry1  32816  fsuppcurry2  32817  resf1o  32822  s2rnOLD  33023  s3rnOLD  33025  cycpmfvlem  33193  cycpmfv3  33196  selvply1rhmlemb  33703  esumfsup  34254  esumpcvgval  34262  esumcvg  34270  esumsup  34273  bnj149  35057  bnj1312  35240  faclimlem1  35971  fullfunfnv  36174  ixpeq1i  36428  cbvixpvw2  36473  knoppcnlem8  36806  knoppcnlem11  36809  mblfinlem2  38025  ovoliunnfl  38029  voliunnfl  38031  subsaliuncl  46801  fcores  47530  isubgr3stgrlem7  48463  isofval2  49522  0funcALT  49578