Theorem fneq1i 5692

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 5686	. 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 189   = wceq 1455   Fn wfn 5596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-fun 5603  df-fn 5604

This theorem is referenced by:  fnunsn  5705  mptfnf  5721  fnopabg  5723  f1oun  5856  f1oi  5873  f1osn  5875  ovid  6440  curry1  6915  curry2  6918  wfrlem5  7066  wfrlem13  7074  tfrlem10  7131  tfr1  7141  seqomlem2  7194  seqomlem3  7195  seqomlem4  7196  fnseqom  7198  unblem4  7852  r1fnon  8264  alephfnon  8522  alephfplem4  8564  alephfp  8565  cfsmolem  8726  infpssrlem3  8761  compssiso  8830  hsmexlem5  8886  axdclem2  8976  wunex2  9189  wuncval2  9198  om2uzrani  12198  om2uzf1oi  12199  uzrdglem  12203  uzrdgfni  12204  uzrdg0i  12205  hashkf  12549  dmaf  15993  cdaf  15994  prdsinvlem  16843  srg1zr  17811  pws1  17893  frlmphl  19388  ovolunlem1  22499  0plef  22679  0pledm  22680  itg1ge0  22693  itg1addlem4  22706  mbfi1fseqlem5  22726  itg2addlem  22765  qaa  23328  2trllemD  25336  eupap1  25753  ghgrpOLD  26145  0vfval  26274  xrge0pluscn  28795  bnj927  29629  bnj535  29750  frrlem5  30567  fullfunfnv  30762  neibastop2lem  31065  fourierdlem42  38050  fourierdlem42OLD  38051  rngcrescrhm  40360  rngcrescrhmALTV  40379