Theorem fneq2i 6630

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   Fn wfn 6528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-fn 6536

This theorem is used by:  fnunop  6648  fnprb  7207  fntpb  7208  fnsuppeq0  8190  tpos0  8254  dfixp  8906  ordtypelem4  9493  imadomnum  10538  ser0f  14119  0csh0  14864  s3fn  14982  prodf1f  15981  efcvgfsum  16172  prmrec  17014  fnpr2o  17643  0ssc  17926  0subcat  17927  mulgfvi  19196  ovolunlem1  25725  volsup  25784  mtest  26640  mtestbdd  26641  pserulm  26658  pserdvlem2  26664  emcllem5  27236  lgamgulm2  27272  lgamcvglem  27276  gamcvg2lem  27295  tglnfn  28889  tgplnfn  29132  crctcshlem4  30288  fsuppcurry1  33195  fsuppcurry2  33196  resf1o  33201  cycpmfvlem  33552  cycpmfv3  33555  selvply1rhmlemb  34029  esumfsup  34580  esumpcvgval  34588  esumcvg  34596  esumsup  34599  bnj149  35384  bnj1312  35567  faclimlem1  36322  fullfunfnv  36525  ixpeq1i  36820  cbvixpvw2  36865  knoppcnlem8  37197  knoppcnlem11  37200  mblfinlem2  38407  ovoliunnfl  38411  voliunnfl  38413  subsaliuncl  47186  fcores  47955  isubgr3stgrlem7  48888  isofval2  49958  0funcALT  50014