Theorem fneq2i 6665

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

Syntax hints:   ↔ wb 206   = wceq 1539   Fn wfn 6555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

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

This theorem is referenced by:  fnunop  6683  fnprb  7229  fntpb  7230  fnsuppeq0  8218  tpos0  8282  wfrlem5OLD  8354  dfixp  8940  ordtypelem4  9562  ser0f  14097  0csh0  14832  s3fn  14951  prodf1f  15929  efcvgfsum  16123  prmrec  16961  fnpr2o  17603  0ssc  17883  0subcat  17884  mulgfvi  19092  ovolunlem1  25533  volsup  25592  mtest  26448  mtestbdd  26449  pserulm  26466  pserdvlem2  26473  emcllem5  27044  lgamgulm2  27080  lgamcvglem  27084  gamcvg2lem  27103  tglnfn  28556  crctcshlem4  29841  fsuppcurry1  32737  fsuppcurry2  32738  resf1o  32742  s2rnOLD  32929  s3rnOLD  32931  cycpmfvlem  33133  cycpmfv3  33136  esumfsup  34072  esumpcvgval  34080  esumcvg  34088  esumsup  34091  bnj149  34890  bnj1312  35073  faclimlem1  35744  fullfunfnv  35948  ixpeq1i  36202  cbvixpvw2  36247  knoppcnlem8  36502  knoppcnlem11  36505  mblfinlem2  37666  ovoliunnfl  37670  voliunnfl  37672  subsaliuncl  46378  fcores  47084  isubgr3stgrlem7  47944  0funcALT  48937