Theorem fneq2i 5986

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

Syntax hints:   ↔ wb 196   = wceq 1483   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fn 5891

This theorem is referenced by:  fnunsn  5998  fnprb  6472  fntpb  6473  fnsuppeq0  7323  tpos0  7382  wfrlem5  7419  dfixp  7910  ordtypelem4  8426  ser0f  12854  0csh0  13539  s3fn  13656  prodf1f  14624  efcvgfsum  14816  prmrec  15626  xpscfn  16219  0ssc  16497  0subcat  16498  mulgfvi  17545  ovolunlem1  23265  volsup  23324  mtest  24158  mtestbdd  24159  pserulm  24176  pserdvlem2  24182  emcllem5  24726  lgamgulm2  24762  lgamcvglem  24766  gamcvg2lem  24785  tglnfn  25442  crctcshlem4  26712  resf1o  29505  esumfsup  30132  esumpcvgval  30140  esumcvg  30148  esumsup  30151  bnj149  30945  bnj1312  31126  faclimlem1  31629  frrlem5  31784  fullfunfnv  32053  knoppcnlem8  32490  knoppcnlem11  32493  mblfinlem2  33447  ovoliunnfl  33451  voliunnfl  33453  subsaliuncl  40576