Theorem fneq2i 6437

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

Syntax hints:   ↔ wb 208   = wceq 1537   Fn wfn 6336

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814  df-fn 6344

This theorem is referenced by:  fnunsn  6450  fnprb  6957  fntpb  6958  fnsuppeq0  7844  tpos0  7908  wfrlem5  7945  dfixp  8449  ordtypelem4  8971  ser0f  13413  0csh0  14140  s3fn  14258  prodf1f  15233  efcvgfsum  15424  prmrec  16241  fnpr2o  16813  0ssc  17090  0subcat  17091  mulgfvi  18213  ovolunlem1  24081  volsup  24140  mtest  24978  mtestbdd  24979  pserulm  24996  pserdvlem2  25002  emcllem5  25563  lgamgulm2  25599  lgamcvglem  25603  gamcvg2lem  25622  tglnfn  26319  crctcshlem4  27584  fsuppcurry1  30447  fsuppcurry2  30448  resf1o  30452  s2rn  30606  s3rn  30608  cycpmfvlem  30761  cycpmfv3  30764  esumfsup  31336  esumpcvgval  31344  esumcvg  31352  esumsup  31355  bnj149  32154  bnj1312  32337  faclimlem1  32982  fullfunfnv  33414  knoppcnlem8  33846  knoppcnlem11  33849  mblfinlem2  34964  ovoliunnfl  34968  voliunnfl  34970  subsaliuncl  42731