Theorem fneq2i 6635

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

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

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 2733

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

This theorem is used by:  fnunop  6653  fnprb  7212  fntpb  7213  fnsuppeq0  8202  tpos0  8266  dfixp  8920  ordtypelem4  9508  imadomnum  10607  ser0f  14191  0csh0  14937  s3fn  15055  prodf1f  16054  efcvgfsum  16245  prmrec  17093  fnpr2o  17722  0ssc  18005  0subcat  18006  mulgfvi  19276  ovolunlem1  25811  volsup  25870  mtest  26724  mtestbdd  26725  pserulm  26742  pserdvlem2  26748  emcllem5  27320  lgamgulm2  27356  lgamcvglem  27360  gamcvg2lem  27379  tglnfn  29003  tgplnfn  29246  crctcshlem4  30402  fsuppcurry1  33309  fsuppcurry2  33310  resf1o  33315  cycpmfvlem  33666  cycpmfv3  33669  selvply1rhmlemb  34144  esumfsup  34695  esumpcvgval  34703  esumcvg  34711  esumsup  34714  bnj149  35498  bnj1312  35681  faclimlem1  36487  fullfunfnv  36690  ixpeq1i  36969  cbvixpvw2  37014  knoppcnlem8  37346  knoppcnlem11  37349  mblfinlem2  38556  ovoliunnfl  38560  voliunnfl  38562  subsaliuncl  47337  fcores  48106  isubgr3stgrlem7  49039  isofval2  50109  0funcALT  50165