Theorem fneq2i 6667

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  fnunop  6685  fnprb  7245  fntpb  7246  fnsuppeq0  8247  tpos0  8311  dfixp  8965  ordtypelem4  9552  imadomnum  10653  ser0f  14238  0csh0  14986  s3fn  15105  prodf1f  16105  efcvgfsum  16296  prmrec  17144  fnpr2o  17779  0ssc  18062  0subcat  18063  mulgfvi  19333  ovolunlem1  25873  volsup  25932  mtest  26788  mtestbdd  26789  pserulm  26806  pserdvlem2  26812  emcllem5  27384  lgamgulm2  27420  lgamcvglem  27424  gamcvg2lem  27443  tglnfn  29067  tgplnfn  29310  crctcshlem4  30466  fsuppcurry1  33412  fsuppcurry2  33413  resf1o  33418  cycpmfvlem  33772  cycpmfv3  33775  selvply1rhmlemb  34262  esumfsup  34813  esumpcvgval  34821  esumcvg  34829  esumsup  34832  bnj149  35616  bnj1312  35799  faclimlem1  36723  fullfunfnv  36925  ixpeq1i  37204  cbvixpvw2  37249  knoppcnlem8  37581  knoppcnlem11  37584  mblfinlem2  38844  ovoliunnfl  38848  voliunnfl  38850  subsaliuncl  47641  fcores  48410  isubgr3stgrlem7  49343  isofval2  50477  0funcALT  50534