Theorem fneq2i 6590

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

Syntax hints:   ↔ wb 206   = wceq 1542   Fn wfn 6487

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-fn 6495

This theorem is referenced by:  fnunop  6608  fnprb  7156  fntpb  7157  fnsuppeq0  8135  tpos0  8199  dfixp  8840  ordtypelem4  9429  ser0f  14008  0csh0  14746  s3fn  14864  prodf1f  15848  efcvgfsum  16042  prmrec  16884  fnpr2o  17512  0ssc  17795  0subcat  17796  mulgfvi  19040  ovolunlem1  25474  volsup  25533  mtest  26382  mtestbdd  26383  pserulm  26400  pserdvlem2  26406  emcllem5  26977  lgamgulm2  27013  lgamcvglem  27017  gamcvg2lem  27036  tglnfn  28629  crctcshlem4  29903  fsuppcurry1  32812  fsuppcurry2  32813  resf1o  32818  s2rnOLD  33019  s3rnOLD  33021  cycpmfvlem  33188  cycpmfv3  33191  esumfsup  34230  esumpcvgval  34238  esumcvg  34246  esumsup  34249  bnj149  35033  bnj1312  35216  faclimlem1  35941  fullfunfnv  36144  ixpeq1i  36398  cbvixpvw2  36443  knoppcnlem8  36776  knoppcnlem11  36779  mblfinlem2  37993  ovoliunnfl  37997  voliunnfl  37999  subsaliuncl  46804  fcores  47527  isubgr3stgrlem7  48460  isofval2  49519  0funcALT  49575