Theorem fneq2i 6667

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

Syntax hints:   ↔ wb 206   = wceq 1537   Fn wfn 6558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-fn 6566

This theorem is referenced by:  fnunop  6685  fnprb  7228  fntpb  7229  fnsuppeq0  8216  tpos0  8280  wfrlem5OLD  8352  dfixp  8938  ordtypelem4  9559  ser0f  14093  0csh0  14828  s3fn  14947  prodf1f  15925  efcvgfsum  16119  prmrec  16956  fnpr2o  17604  0ssc  17888  0subcat  17889  mulgfvi  19104  ovolunlem1  25546  volsup  25605  mtest  26462  mtestbdd  26463  pserulm  26480  pserdvlem2  26487  emcllem5  27058  lgamgulm2  27094  lgamcvglem  27098  gamcvg2lem  27117  tglnfn  28570  crctcshlem4  29850  fsuppcurry1  32743  fsuppcurry2  32744  resf1o  32748  s2rnOLD  32913  s3rnOLD  32915  cycpmfvlem  33115  cycpmfv3  33118  esumfsup  34051  esumpcvgval  34059  esumcvg  34067  esumsup  34070  bnj149  34868  bnj1312  35051  faclimlem1  35723  fullfunfnv  35928  ixpeq1i  36182  cbvixpvw2  36228  knoppcnlem8  36483  knoppcnlem11  36486  mblfinlem2  37645  ovoliunnfl  37649  voliunnfl  37651  subsaliuncl  46314  fcores  47017  isubgr3stgrlem7  47875