Theorem fneq2i 6627

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

Syntax hints:   ↔ wb 205   = wceq 1541   Fn wfn 6518

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723  df-fn 6526

This theorem is referenced by:  fnunop  6643  fnprb  7185  fntpb  7186  fnsuppeq0  8150  tpos0  8214  wfrlem5OLD  8286  dfixp  8866  ordtypelem4  9488  ser0f  13993  0csh0  14715  s3fn  14834  prodf1f  15810  efcvgfsum  16001  prmrec  16827  fnpr2o  17475  0ssc  17759  0subcat  17760  mulgfvi  18914  ovolunlem1  24920  volsup  24979  mtest  25822  mtestbdd  25823  pserulm  25840  pserdvlem2  25846  emcllem5  26408  lgamgulm2  26444  lgamcvglem  26448  gamcvg2lem  26467  tglnfn  27593  crctcshlem4  28869  fsuppcurry1  31751  fsuppcurry2  31752  resf1o  31756  s2rn  31911  s3rn  31913  cycpmfvlem  32072  cycpmfv3  32075  esumfsup  32799  esumpcvgval  32807  esumcvg  32815  esumsup  32818  bnj149  33617  bnj1312  33800  faclimlem1  34443  fullfunfnv  34648  knoppcnlem8  35080  knoppcnlem11  35083  mblfinlem2  36230  ovoliunnfl  36234  voliunnfl  36236  subsaliuncl  44759  fcores  45461