Theorem fneq1i 6597

Description: Equality inference for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq1i.1	⊢ 𝐹 = 𝐺

Assertion

Ref	Expression
fneq1i	⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Proof of Theorem fneq1i

Step	Hyp	Ref	Expression
1		fneq1i.1	. 2 ⊢ 𝐹 = 𝐺
2		fneq1 6591	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	ax-mp 5	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴)

Syntax hints:   ↔ wb 206   = wceq 1542   Fn wfn 6495

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-fun 6502  df-fn 6503

This theorem is referenced by:  fnunop  6616  mptfnf  6635  fnopabg  6637  f1oun  6801  f1oiOLD  6821  f1osn  6823  ovid  7509  curry1  8056  curry2  8059  fsplitfpar  8070  frrlem11  8248  tfrlem10  8328  tfr1  8338  seqomlem2  8392  seqomlem3  8393  seqomlem4  8394  fnseqom  8396  unblem4  9207  r1fnon  9691  alephfnon  9987  alephfplem4  10029  alephfp  10030  cfsmolem  10192  infpssrlem3  10227  compssiso  10296  hsmexlem5  10352  axdclem2  10442  wunex2  10661  wuncval2  10670  om2uzrani  13887  om2uzf1oi  13888  uzrdglem  13892  uzrdgfni  13893  uzrdg0i  13894  hashkf  14267  dmaf  17985  cdaf  17986  prdsinvlem  18991  srg1zr  20162  pws1  20272  rngcrescrhm  20629  frlmphl  21748  ovolunlem1  25466  0plef  25641  0pledm  25642  itg1ge0  25655  mbfi1fseqlem5  25688  itg2addlem  25727  qaa  26299  precsexlem1  28215  precsexlem2  28216  precsexlem3  28217  precsexlem4  28218  precsexlem5  28219  ex-fpar  30549  0vfval  30693  xrge0pluscn  34117  bnj927  34945  bnj535  35065  fullfunfnv  36159  neibastop2lem  36573  fnmptif  45620  fourierdlem42  46504  cjnpoly  47246  fcoreslem4  47423  upgrimwlklem1  48254  rngcrescrhmALTV  48637  isofval2  49388