Theorem fneq2i 6531

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

Syntax hints:   ↔ wb 205   = wceq 1539   Fn wfn 6428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-fn 6436

This theorem is referenced by:  fnunop  6547  fnprb  7084  fntpb  7085  fnsuppeq0  8008  tpos0  8072  wfrlem5OLD  8144  dfixp  8687  ordtypelem4  9280  ser0f  13776  0csh0  14506  s3fn  14624  prodf1f  15604  efcvgfsum  15795  prmrec  16623  fnpr2o  17268  0ssc  17552  0subcat  17553  mulgfvi  18706  ovolunlem1  24661  volsup  24720  mtest  25563  mtestbdd  25564  pserulm  25581  pserdvlem2  25587  emcllem5  26149  lgamgulm2  26185  lgamcvglem  26189  gamcvg2lem  26208  tglnfn  26908  crctcshlem4  28185  fsuppcurry1  31060  fsuppcurry2  31061  resf1o  31065  s2rn  31218  s3rn  31220  cycpmfvlem  31379  cycpmfv3  31382  esumfsup  32038  esumpcvgval  32046  esumcvg  32054  esumsup  32057  bnj149  32855  bnj1312  33038  faclimlem1  33709  fullfunfnv  34248  knoppcnlem8  34680  knoppcnlem11  34683  mblfinlem2  35815  ovoliunnfl  35819  voliunnfl  35821  subsaliuncl  43897  fcores  44561