Theorem fneq2i 6024

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

Syntax hints:   ↔ wb 196   = wceq 1523   Fn wfn 5921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-fn 5929

This theorem is referenced by:  fnunsn  6036  fnprb  6513  fntpb  6514  fnsuppeq0  7368  tpos0  7427  wfrlem5  7464  dfixp  7952  ordtypelem4  8467  ser0f  12894  0csh0  13585  s3fn  13702  prodf1f  14668  efcvgfsum  14860  prmrec  15673  xpscfn  16266  0ssc  16544  0subcat  16545  mulgfvi  17592  ovolunlem1  23311  volsup  23370  mtest  24203  mtestbdd  24204  pserulm  24221  pserdvlem2  24227  emcllem5  24771  lgamgulm2  24807  lgamcvglem  24811  gamcvg2lem  24830  tglnfn  25487  crctcshlem4  26768  resf1o  29633  esumfsup  30260  esumpcvgval  30268  esumcvg  30276  esumsup  30279  bnj149  31071  bnj1312  31252  faclimlem1  31755  frrlem5  31909  fullfunfnv  32178  knoppcnlem8  32615  knoppcnlem11  32618  mblfinlem2  33577  ovoliunnfl  33581  voliunnfl  33583  subsaliuncl  40894