Theorem fneq1i 5684

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 5678	. 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 187   = wceq 1437   Fn wfn 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-rab 2784  df-v 3083  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-br 4421  df-opab 4480  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-fun 5599  df-fn 5600

This theorem is referenced by:  fnunsn  5697  mptfnf  5713  fnopabg  5715  f1oun  5846  f1oi  5862  f1osn  5864  ovid  6423  curry1  6895  curry2  6898  wfrlem5  7044  wfrlem13  7052  tfrlem10  7109  tfr1  7119  seqomlem2  7172  seqomlem3  7173  seqomlem4  7174  fnseqom  7176  unblem4  7828  r1fnon  8239  alephfnon  8496  alephfplem4  8538  alephfp  8539  cfsmolem  8700  infpssrlem3  8735  compssiso  8804  hsmexlem5  8860  axdclem2  8950  wunex2  9163  wuncval2  9172  om2uzrani  12165  om2uzf1oi  12166  uzrdglem  12170  uzrdgfni  12171  uzrdg0i  12172  hashkf  12516  dmaf  15931  cdaf  15932  prdsinvlem  16781  srg1zr  17749  pws1  17831  frlmphl  19325  ovolunlem1  22436  0plef  22616  0pledm  22617  itg1ge0  22630  itg1addlem4  22643  mbfi1fseqlem5  22663  itg2addlem  22702  qaa  23265  2trllemD  25272  eupap1  25689  ghgrpOLD  26081  0vfval  26210  xrge0pluscn  28741  bnj927  29575  bnj535  29696  frrlem5  30512  fullfunfnv  30705  neibastop2lem  31008  fourierdlem42  37831  fourierdlem42OLD  37832  rngcrescrhm  39358  rngcrescrhmALTV  39377