Theorem fneq2i 6328

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

Syntax hints:   ↔ wb 207   = wceq 1525   Fn wfn 6227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-9 2093  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1766  df-cleq 2790  df-fn 6235

This theorem is referenced by:  fnunsn  6341  fnprb  6844  fntpb  6845  fnsuppeq0  7716  tpos0  7780  wfrlem5  7818  dfixp  8319  ordtypelem4  8838  ser0f  13277  0csh0  13995  s3fn  14113  prodf1f  15085  efcvgfsum  15276  prmrec  16091  fnpr2o  16663  0ssc  16940  0subcat  16941  mulgfvi  17991  ovolunlem1  23785  volsup  23844  mtest  24679  mtestbdd  24680  pserulm  24697  pserdvlem2  24703  emcllem5  25263  lgamgulm2  25299  lgamcvglem  25303  gamcvg2lem  25322  tglnfn  26019  crctcshlem4  27284  fsuppcurry1  30145  fsuppcurry2  30146  resf1o  30150  s2rn  30296  s3rn  30298  cycpmfvlem  30397  cycpmfv3  30400  esumfsup  30942  esumpcvgval  30950  esumcvg  30958  esumsup  30961  bnj149  31759  bnj1312  31940  faclimlem1  32585  fullfunfnv  33018  knoppcnlem8  33450  knoppcnlem11  33453  mblfinlem2  34482  ovoliunnfl  34486  voliunnfl  34488  subsaliuncl  42205