Theorem fneq2i 6641

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

Syntax hints:   ↔ wb 206   = wceq 1540   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  fnunop  6659  fnprb  7205  fntpb  7206  fnsuppeq0  8196  tpos0  8260  wfrlem5OLD  8332  dfixp  8918  ordtypelem4  9540  ser0f  14078  0csh0  14816  s3fn  14935  prodf1f  15913  efcvgfsum  16107  prmrec  16947  fnpr2o  17576  0ssc  17855  0subcat  17856  mulgfvi  19061  ovolunlem1  25455  volsup  25514  mtest  26370  mtestbdd  26371  pserulm  26388  pserdvlem2  26395  emcllem5  26967  lgamgulm2  27003  lgamcvglem  27007  gamcvg2lem  27026  tglnfn  28531  crctcshlem4  29807  fsuppcurry1  32707  fsuppcurry2  32708  resf1o  32712  s2rnOLD  32924  s3rnOLD  32926  cycpmfvlem  33128  cycpmfv3  33131  esumfsup  34106  esumpcvgval  34114  esumcvg  34122  esumsup  34125  bnj149  34911  bnj1312  35094  faclimlem1  35765  fullfunfnv  35969  ixpeq1i  36223  cbvixpvw2  36268  knoppcnlem8  36523  knoppcnlem11  36526  mblfinlem2  37687  ovoliunnfl  37691  voliunnfl  37693  subsaliuncl  46354  fcores  47063  isubgr3stgrlem7  47951  isofval2  48969  0funcALT  49020