Theorem fneq2i 6614

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

Syntax hints:   ↔ wb 208   = wceq 1559   Fn wfn 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-fn 6519

This theorem is referenced by:  fnunop  6632  fnprb  7187  fntpb  7188  fnsuppeq0  8166  tpos0  8230  dfixp  8875  ordtypelem4  9463  ser0f  14062  0csh0  14800  s3fn  14918  prodf1f  15913  efcvgfsum  16107  prmrec  16949  fnpr2o  17578  0ssc  17861  0subcat  17862  mulgfvi  19106  ovolunlem1  25547  volsup  25606  mtest  26455  mtestbdd  26456  pserulm  26473  pserdvlem2  26479  emcllem5  27052  lgamgulm2  27088  lgamcvglem  27092  gamcvg2lem  27111  tglnfn  28704  crctcshlem4  29977  fsuppcurry1  32887  fsuppcurry2  32888  resf1o  32893  s2rnOLD  33083  s3rnOLD  33085  cycpmfvlem  33253  cycpmfv3  33256  selvply1rhmlemb  33777  esumfsup  34328  esumpcvgval  34336  esumcvg  34344  esumsup  34347  bnj149  35131  bnj1312  35314  faclimlem1  36054  fullfunfnv  36257  ixpeq1i  36521  cbvixpvw2  36566  knoppcnlem8  36899  knoppcnlem11  36902  mblfinlem2  38118  ovoliunnfl  38122  voliunnfl  38124  subsaliuncl  46893  fcores  47622  isubgr3stgrlem7  48555  isofval2  49614  0funcALT  49670