Theorem fneq2i 6588

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

Syntax hints:   ↔ wb 206   = wceq 1542   Fn wfn 6485

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6493

This theorem is referenced by:  fnunop  6606  fnprb  7154  fntpb  7155  fnsuppeq0  8133  tpos0  8197  dfixp  8838  ordtypelem4  9427  ser0f  13979  0csh0  14717  s3fn  14835  prodf1f  15816  efcvgfsum  16010  prmrec  16851  fnpr2o  17479  0ssc  17762  0subcat  17763  mulgfvi  19007  ovolunlem1  25442  volsup  25501  mtest  26353  mtestbdd  26354  pserulm  26371  pserdvlem2  26378  emcllem5  26950  lgamgulm2  26986  lgamcvglem  26990  gamcvg2lem  27009  tglnfn  28603  crctcshlem4  29877  fsuppcurry1  32786  fsuppcurry2  32787  resf1o  32792  s2rnOLD  33009  s3rnOLD  33011  cycpmfvlem  33178  cycpmfv3  33181  esumfsup  34220  esumpcvgval  34228  esumcvg  34236  esumsup  34239  bnj149  35023  bnj1312  35206  faclimlem1  35931  fullfunfnv  36134  ixpeq1i  36388  cbvixpvw2  36433  knoppcnlem8  36758  knoppcnlem11  36761  mblfinlem2  37970  ovoliunnfl  37974  voliunnfl  37976  subsaliuncl  46790  fcores  47501  isubgr3stgrlem7  48406  isofval2  49465  0funcALT  49521