Theorem fneq2i 6598

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

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

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 2709

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

This theorem is referenced by:  fnunop  6616  fnprb  7164  fntpb  7165  fnsuppeq0  8144  tpos0  8208  dfixp  8849  ordtypelem4  9438  ser0f  13990  0csh0  14728  s3fn  14846  prodf1f  15827  efcvgfsum  16021  prmrec  16862  fnpr2o  17490  0ssc  17773  0subcat  17774  mulgfvi  19015  ovolunlem1  25466  volsup  25525  mtest  26381  mtestbdd  26382  pserulm  26399  pserdvlem2  26406  emcllem5  26978  lgamgulm2  27014  lgamcvglem  27018  gamcvg2lem  27037  tglnfn  28631  crctcshlem4  29905  fsuppcurry1  32814  fsuppcurry2  32815  resf1o  32820  s2rnOLD  33037  s3rnOLD  33039  cycpmfvlem  33206  cycpmfv3  33209  esumfsup  34248  esumpcvgval  34256  esumcvg  34264  esumsup  34267  bnj149  35051  bnj1312  35234  faclimlem1  35959  fullfunfnv  36162  ixpeq1i  36416  cbvixpvw2  36461  knoppcnlem8  36722  knoppcnlem11  36725  mblfinlem2  37909  ovoliunnfl  37913  voliunnfl  37915  subsaliuncl  46716  fcores  47427  isubgr3stgrlem7  48332  isofval2  49391  0funcALT  49447