Theorem fneq1i 5502

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 5496	. 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 1364   Fn wfn 5410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-fun 5417  df-fn 5418

This theorem is referenced by:  fnunsn  5515  fnopabg  5531  f1oun  5657  f1oi  5673  f1osn  5675  ovid  6206  curry1  6663  curry2  6666  tfrlem10  6842  tfr1  6852  seqomlem2  6902  seqomlem3  6903  seqomlem4  6904  fnseqom  6906  unblem4  7563  r1fnon  7970  alephfnon  8231  alephfplem4  8273  alephfp  8274  cfsmolem  8435  infpssrlem3  8470  compssiso  8539  hsmexlem5  8595  axdclem2  8685  wunex2  8901  wuncval2  8910  om2uzrani  11771  om2uzf1oi  11772  uzrdglem  11776  uzrdgfni  11777  uzrdg0i  11778  hashkf  12101  dmaf  14913  cdaf  14914  prdsinvlem  15656  pws1  16698  frlmphl  18165  ovolunlem1  20939  0plef  21109  0pledm  21110  itg1ge0  21123  itg1addlem4  21136  mbfi1fseqlem5  21156  itg2addlem  21195  qaa  21748  2trllemD  23391  eupap1  23532  ghgrp  23790  0vfval  23919  mptfnf  25911  xrge0pluscn  26306  wfrlem5  27657  wfrlem13  27665  frrlem5  27701  fullfunfnv  27906  neibastop2lem  28506  bnj927  31596  bnj535  31717