Theorem fneq2i 6637

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   Fn wfn 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-fn 6543

This theorem is used by:  fnunop  6655  fnprb  7213  fntpb  7214  fnsuppeq0  8194  tpos0  8258  dfixp  8903  ordtypelem4  9490  ser0f  14109  0csh0  14854  s3fn  14972  prodf1f  15969  efcvgfsum  16162  prmrec  17004  fnpr2o  17633  0ssc  17916  0subcat  17917  mulgfvi  19183  ovolunlem1  25707  volsup  25766  mtest  26618  mtestbdd  26619  pserulm  26636  pserdvlem2  26642  emcllem5  27215  lgamgulm2  27251  lgamcvglem  27255  gamcvg2lem  27274  tglnfn  28867  tgplnfn  29108  crctcshlem4  30236  fsuppcurry1  33139  fsuppcurry2  33140  resf1o  33145  cycpmfvlem  33496  cycpmfv3  33499  selvply1rhmlemb  33973  esumfsup  34524  esumpcvgval  34532  esumcvg  34540  esumsup  34543  bnj149  35328  bnj1312  35511  faclimlem1  36272  fullfunfnv  36475  ixpeq1i  36769  cbvixpvw2  36814  knoppcnlem8  37146  knoppcnlem11  37149  mblfinlem2  38366  ovoliunnfl  38370  voliunnfl  38372  subsaliuncl  47130  fcores  47862  isubgr3stgrlem7  48795  isofval2  49867  0funcALT  49923