Theorem fneq2i 6598

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

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

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 6502

This theorem is referenced by:  fnunop  6616  fnprb  7164  fntpb  7165  fnsuppeq0  8148  tpos0  8212  dfixp  8849  ordtypelem4  9450  ser0f  13996  0csh0  14734  s3fn  14853  prodf1f  15834  efcvgfsum  16028  prmrec  16869  fnpr2o  17496  0ssc  17775  0subcat  17776  mulgfvi  18981  ovolunlem1  25374  volsup  25433  mtest  26289  mtestbdd  26290  pserulm  26307  pserdvlem2  26314  emcllem5  26886  lgamgulm2  26922  lgamcvglem  26926  gamcvg2lem  26945  tglnfn  28450  crctcshlem4  29723  fsuppcurry1  32621  fsuppcurry2  32622  resf1o  32626  s2rnOLD  32838  s3rnOLD  32840  cycpmfvlem  33042  cycpmfv3  33045  esumfsup  34033  esumpcvgval  34041  esumcvg  34049  esumsup  34052  bnj149  34838  bnj1312  35021  faclimlem1  35703  fullfunfnv  35907  ixpeq1i  36161  cbvixpvw2  36206  knoppcnlem8  36461  knoppcnlem11  36464  mblfinlem2  37625  ovoliunnfl  37629  voliunnfl  37631  subsaliuncl  46329  fcores  47041  isubgr3stgrlem7  47944  isofval2  48994  0funcALT  49050