Theorem fneq2i 6515

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

Syntax hints:   ↔ wb 205   = wceq 1539   Fn wfn 6413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-fn 6421

This theorem is referenced by:  fnunop  6531  fnprb  7066  fntpb  7067  fnsuppeq0  7979  tpos0  8043  wfrlem5OLD  8115  dfixp  8645  ordtypelem4  9210  ser0f  13704  0csh0  14434  s3fn  14552  prodf1f  15532  efcvgfsum  15723  prmrec  16551  fnpr2o  17185  0ssc  17468  0subcat  17469  mulgfvi  18621  ovolunlem1  24566  volsup  24625  mtest  25468  mtestbdd  25469  pserulm  25486  pserdvlem2  25492  emcllem5  26054  lgamgulm2  26090  lgamcvglem  26094  gamcvg2lem  26113  tglnfn  26812  crctcshlem4  28086  fsuppcurry1  30962  fsuppcurry2  30963  resf1o  30967  s2rn  31120  s3rn  31122  cycpmfvlem  31281  cycpmfv3  31284  esumfsup  31938  esumpcvgval  31946  esumcvg  31954  esumsup  31957  bnj149  32755  bnj1312  32938  faclimlem1  33615  fullfunfnv  34175  knoppcnlem8  34607  knoppcnlem11  34610  mblfinlem2  35742  ovoliunnfl  35746  voliunnfl  35748  subsaliuncl  43787  fcores  44448