Theorem fneq1i 5517

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 5511	. 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 1369   Fn wfn 5425

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-opab 4363  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-fun 5432  df-fn 5433

This theorem is referenced by:  fnunsn  5530  fnopabg  5546  f1oun  5672  f1oi  5688  f1osn  5690  ovid  6219  curry1  6676  curry2  6679  tfrlem10  6858  tfr1  6868  seqomlem2  6918  seqomlem3  6919  seqomlem4  6920  fnseqom  6922  unblem4  7579  r1fnon  7986  alephfnon  8247  alephfplem4  8289  alephfp  8290  cfsmolem  8451  infpssrlem3  8486  compssiso  8555  hsmexlem5  8611  axdclem2  8701  wunex2  8917  wuncval2  8926  om2uzrani  11787  om2uzf1oi  11788  uzrdglem  11792  uzrdgfni  11793  uzrdg0i  11794  hashkf  12117  dmaf  14929  cdaf  14930  prdsinvlem  15675  pws1  16720  frlmphl  18218  ovolunlem1  20992  0plef  21162  0pledm  21163  itg1ge0  21176  itg1addlem4  21189  mbfi1fseqlem5  21209  itg2addlem  21248  qaa  21801  2trllemD  23468  eupap1  23609  ghgrp  23867  0vfval  23996  mptfnf  25988  xrge0pluscn  26382  wfrlem5  27740  wfrlem13  27748  frrlem5  27784  fullfunfnv  27989  neibastop2lem  28593  bnj927  31774  bnj535  31895