Theorem fneq2i 6616

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

Syntax hints:   ↔ wb 206   = wceq 1540   Fn wfn 6506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-fn 6514

This theorem is referenced by:  fnunop  6634  fnprb  7182  fntpb  7183  fnsuppeq0  8171  tpos0  8235  dfixp  8872  ordtypelem4  9474  ser0f  14020  0csh0  14758  s3fn  14877  prodf1f  15858  efcvgfsum  16052  prmrec  16893  fnpr2o  17520  0ssc  17799  0subcat  17800  mulgfvi  19005  ovolunlem1  25398  volsup  25457  mtest  26313  mtestbdd  26314  pserulm  26331  pserdvlem2  26338  emcllem5  26910  lgamgulm2  26946  lgamcvglem  26950  gamcvg2lem  26969  tglnfn  28474  crctcshlem4  29750  fsuppcurry1  32648  fsuppcurry2  32649  resf1o  32653  s2rnOLD  32865  s3rnOLD  32867  cycpmfvlem  33069  cycpmfv3  33072  esumfsup  34060  esumpcvgval  34068  esumcvg  34076  esumsup  34079  bnj149  34865  bnj1312  35048  faclimlem1  35730  fullfunfnv  35934  ixpeq1i  36188  cbvixpvw2  36233  knoppcnlem8  36488  knoppcnlem11  36491  mblfinlem2  37652  ovoliunnfl  37656  voliunnfl  37658  subsaliuncl  46356  fcores  47065  isubgr3stgrlem7  47968  isofval2  49018  0funcALT  49074