Theorem fneq2i 5900

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

Syntax hints:   ↔ wb 195   = wceq 1475   Fn wfn 5799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807

This theorem is referenced by:  fnunsn  5912  fnprb  6377  fntpb  6378  fnsuppeq0  7210  tpos0  7269  wfrlem5  7306  dfixp  7796  ordtypelem4  8309  ser0f  12716  0csh0  13390  s3fn  13506  prodf1f  14463  efcvgfsum  14655  prmrec  15464  xpscfn  16042  0ssc  16320  0subcat  16321  mulgfvi  17368  ovolunlem1  23072  volsup  23131  mtest  23962  mtestbdd  23963  pserulm  23980  pserdvlem2  23986  emcllem5  24526  lgamgulm2  24562  lgamcvglem  24566  gamcvg2lem  24585  tglnfn  25242  resf1o  28893  esumfsup  29459  esumpcvgval  29467  esumcvg  29475  esumsup  29478  bnj149  30199  bnj1312  30380  faclimlem1  30882  frrlem5  31028  fullfunfnv  31223  knoppcnlem8  31660  knoppcnlem11  31663  mblfinlem2  32617  ovoliunnfl  32621  voliunnfl  32623  subsaliuncl  39252  crctcshlem4  41023