Theorem fneq1i 6595

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6500  df-fn 6501

This theorem is referenced by:  fnunop  6614  mptfnf  6633  fnopabg  6635  f1oun  6799  f1oiOLD  6819  f1osn  6821  ovid  7508  curry1  8054  curry2  8057  fsplitfpar  8068  frrlem11  8246  tfrlem10  8326  tfr1  8336  seqomlem2  8390  seqomlem3  8391  seqomlem4  8392  fnseqom  8394  unblem4  9205  r1fnon  9691  alephfnon  9987  alephfplem4  10029  alephfp  10030  cfsmolem  10192  infpssrlem3  10227  compssiso  10296  hsmexlem5  10352  axdclem2  10442  wunex2  10661  wuncval2  10670  om2uzrani  13914  om2uzf1oi  13915  uzrdglem  13919  uzrdgfni  13920  uzrdg0i  13921  hashkf  14294  dmaf  18016  cdaf  18017  prdsinvlem  19025  srg1zr  20196  pws1  20304  rngcrescrhm  20661  frlmphl  21761  ovolunlem1  25464  0plef  25639  0pledm  25640  itg1ge0  25653  mbfi1fseqlem5  25686  itg2addlem  25725  qaa  26289  precsexlem1  28199  precsexlem2  28200  precsexlem3  28201  precsexlem4  28202  precsexlem5  28203  ex-fpar  30532  0vfval  30677  xrge0pluscn  34084  bnj927  34912  bnj535  35032  fullfunfnv  36128  neibastop2lem  36542  fnmptif  45694  fourierdlem42  46577  cjnpoly  47337  fcoreslem4  47514  upgrimwlklem1  48373  rngcrescrhmALTV  48756  isofval2  49507