Theorem fneq2i 6590

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

Syntax hints:   ↔ wb 206   = wceq 1541   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  fnunop  6608  fnprb  7154  fntpb  7155  fnsuppeq0  8134  tpos0  8198  dfixp  8837  ordtypelem4  9426  ser0f  13978  0csh0  14716  s3fn  14834  prodf1f  15815  efcvgfsum  16009  prmrec  16850  fnpr2o  17478  0ssc  17761  0subcat  17762  mulgfvi  19003  ovolunlem1  25454  volsup  25513  mtest  26369  mtestbdd  26370  pserulm  26387  pserdvlem2  26394  emcllem5  26966  lgamgulm2  27002  lgamcvglem  27006  gamcvg2lem  27025  tglnfn  28619  crctcshlem4  29893  fsuppcurry1  32803  fsuppcurry2  32804  resf1o  32809  s2rnOLD  33026  s3rnOLD  33028  cycpmfvlem  33194  cycpmfv3  33197  esumfsup  34227  esumpcvgval  34235  esumcvg  34243  esumsup  34246  bnj149  35031  bnj1312  35214  faclimlem1  35937  fullfunfnv  36140  ixpeq1i  36394  cbvixpvw2  36439  knoppcnlem8  36700  knoppcnlem11  36703  mblfinlem2  37859  ovoliunnfl  37863  voliunnfl  37865  subsaliuncl  46602  fcores  47313  isubgr3stgrlem7  48218  isofval2  49277  0funcALT  49333