Theorem fneq2i 6432

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

Syntax hints:   ↔ wb 209   = wceq 1538   Fn wfn 6330

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2729

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2750  df-fn 6338

This theorem is referenced by:  fnunop  6447  fnprb  6962  fntpb  6963  fnsuppeq0  7866  tpos0  7932  wfrlem5  7969  dfixp  8481  ordtypelem4  9018  ser0f  13473  0csh0  14202  s3fn  14320  prodf1f  15296  efcvgfsum  15487  prmrec  16313  fnpr2o  16888  0ssc  17166  0subcat  17167  mulgfvi  18297  ovolunlem1  24197  volsup  24256  mtest  25098  mtestbdd  25099  pserulm  25116  pserdvlem2  25122  emcllem5  25684  lgamgulm2  25720  lgamcvglem  25724  gamcvg2lem  25743  tglnfn  26440  crctcshlem4  27705  fsuppcurry1  30584  fsuppcurry2  30585  resf1o  30589  s2rn  30742  s3rn  30744  cycpmfvlem  30905  cycpmfv3  30908  esumfsup  31557  esumpcvgval  31565  esumcvg  31573  esumsup  31576  bnj149  32375  bnj1312  32558  faclimlem1  33224  fullfunfnv  33797  knoppcnlem8  34229  knoppcnlem11  34232  mblfinlem2  35375  ovoliunnfl  35379  voliunnfl  35381  subsaliuncl  43364