Theorem fneq2i 6633

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

Syntax hints:   ↔ wb 209   = wceq 1570   Fn wfn 6531

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6539

This theorem is referenced by:  fnunop  6651  fnprb  7206  fntpb  7207  fnsuppeq0  8184  tpos0  8248  dfixp  8893  ordtypelem4  9479  ser0f  14087  0csh0  14826  s3fn  14944  prodf1f  15942  efcvgfsum  16135  prmrec  16977  fnpr2o  17606  0ssc  17889  0subcat  17890  mulgfvi  19134  ovolunlem1  25656  volsup  25715  mtest  26567  mtestbdd  26568  pserulm  26585  pserdvlem2  26591  emcllem5  27164  lgamgulm2  27200  lgamcvglem  27204  gamcvg2lem  27223  tglnfn  28816  tgplnfn  29057  crctcshlem4  30169  fsuppcurry1  33069  fsuppcurry2  33070  resf1o  33075  s2rnOLD  33264  s3rnOLD  33266  cycpmfvlem  33432  cycpmfv3  33435  selvply1rhmlemb  33909  esumfsup  34460  esumpcvgval  34468  esumcvg  34476  esumsup  34479  bnj149  35263  bnj1312  35446  faclimlem1  36235  fullfunfnv  36438  ixpeq1i  36712  cbvixpvw2  36757  knoppcnlem8  37089  knoppcnlem11  37092  mblfinlem2  38309  ovoliunnfl  38313  voliunnfl  38315  subsaliuncl  47072  fcores  47804  isubgr3stgrlem7  48737  isofval2  49810  0funcALT  49866