Theorem fneq2i 6596

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

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

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 2708

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

This theorem is referenced by:  fnunop  6614  fnprb  7163  fntpb  7164  fnsuppeq0  8142  tpos0  8206  dfixp  8847  ordtypelem4  9436  ser0f  14017  0csh0  14755  s3fn  14873  prodf1f  15857  efcvgfsum  16051  prmrec  16893  fnpr2o  17521  0ssc  17804  0subcat  17805  mulgfvi  19049  ovolunlem1  25464  volsup  25523  mtest  26369  mtestbdd  26370  pserulm  26387  pserdvlem2  26393  emcllem5  26963  lgamgulm2  26999  lgamcvglem  27003  gamcvg2lem  27022  tglnfn  28615  crctcshlem4  29888  fsuppcurry1  32797  fsuppcurry2  32798  resf1o  32803  s2rnOLD  33004  s3rnOLD  33006  cycpmfvlem  33173  cycpmfv3  33176  esumfsup  34214  esumpcvgval  34222  esumcvg  34230  esumsup  34233  bnj149  35017  bnj1312  35200  faclimlem1  35925  fullfunfnv  36128  ixpeq1i  36382  cbvixpvw2  36427  knoppcnlem8  36760  knoppcnlem11  36763  mblfinlem2  37979  ovoliunnfl  37983  voliunnfl  37985  subsaliuncl  46786  fcores  47515  isubgr3stgrlem7  48448  isofval2  49507  0funcALT  49563