Theorem fneq1i 5583

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

Hypothesis

Ref	Expression
fneq1i.1	|- F = G

Assertion

Ref	Expression
fneq1i	|- ( F Fn A <-> G Fn A )

Proof of Theorem fneq1i

Step	Hyp	Ref	Expression
1		fneq1i.1	. 2 |- F = G
2		fneq1 5577	. 2 |- ( F = G -> ( F Fn A <-> G Fn A ) )
3	1, 2	ax-mp 5	1 |- ( F Fn A <-> G Fn A )

Syntax hints:   <-> wb 184   = wceq 1399   Fn wfn 5491

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-br 4368  df-opab 4426  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-fun 5498  df-fn 5499

This theorem is referenced by:  fnunsn  5596  fnopabg  5612  f1oun  5743  f1oi  5759  f1osn  5761  ovid  6318  curry1  6791  curry2  6794  tfrlem10  6974  tfr1  6984  seqomlem2  7034  seqomlem3  7035  seqomlem4  7036  fnseqom  7038  unblem4  7690  r1fnon  8098  alephfnon  8359  alephfplem4  8401  alephfp  8402  cfsmolem  8563  infpssrlem3  8598  compssiso  8667  hsmexlem5  8723  axdclem2  8813  wunex2  9027  wuncval2  9036  om2uzrani  11966  om2uzf1oi  11967  uzrdglem  11971  uzrdgfni  11972  uzrdg0i  11973  hashkf  12309  dmaf  15445  cdaf  15446  prdsinvlem  16295  srg1zr  17293  pws1  17378  frlmphl  18901  ovolunlem1  21993  0plef  22164  0pledm  22165  itg1ge0  22178  itg1addlem4  22191  mbfi1fseqlem5  22211  itg2addlem  22250  qaa  22804  2trllemD  24680  eupap1  25097  ghgrpOLD  25487  0vfval  25616  mptfnf  27640  xrge0pluscn  28076  wfrlem5  29512  wfrlem13  29520  frrlem5  29556  fullfunfnv  29749  neibastop2lem  30344  fourierdlem42  32097  rngcrescrhm  33093  rngcrescrhmALTV  33112  bnj927  34174  bnj535  34295