Theorem fneq2i 6634

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

Syntax hints:   ↔ wb 209   = wceq 1567   Fn wfn 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-fn 6540

This theorem is referenced by:  fnunop  6652  fnprb  7207  fntpb  7208  fnsuppeq0  8187  tpos0  8251  dfixp  8896  ordtypelem4  9482  ser0f  14090  0csh0  14829  s3fn  14947  prodf1f  15945  efcvgfsum  16139  prmrec  16981  fnpr2o  17610  0ssc  17893  0subcat  17894  mulgfvi  19138  ovolunlem1  25624  volsup  25683  mtest  26532  mtestbdd  26533  pserulm  26550  pserdvlem2  26556  emcllem5  27129  lgamgulm2  27165  lgamcvglem  27169  gamcvg2lem  27188  tglnfn  28781  tgplnfn  29014  crctcshlem4  30109  fsuppcurry1  33009  fsuppcurry2  33010  resf1o  33015  s2rnOLD  33204  s3rnOLD  33206  cycpmfvlem  33372  cycpmfv3  33375  selvply1rhmlemb  33853  esumfsup  34404  esumpcvgval  34412  esumcvg  34420  esumsup  34423  bnj149  35207  bnj1312  35390  faclimlem1  36133  fullfunfnv  36336  ixpeq1i  36600  cbvixpvw2  36645  knoppcnlem8  36977  knoppcnlem11  36980  mblfinlem2  38196  ovoliunnfl  38200  voliunnfl  38202  subsaliuncl  46963  fcores  47692  isubgr3stgrlem7  48625  isofval2  49694  0funcALT  49750