Theorem fneq1 5270

Description: Equality theorem for function predicate with domain. (Contributed by NM, 1-Aug-1994.)

Assertion

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

Proof of Theorem fneq1

Step	Hyp	Ref	Expression
1		funeq 5202	. . 3 |- ( F = G -> ( Fun F <-> Fun G ) )
2		dmeq 4798	. . . 4 |- ( F = G -> dom F = dom G )
3	2	eqeq1d 2173	. . 3 |- ( F = G -> ( dom F = A <-> dom G = A ) )
4	1, 3	anbi12d 465	. 2 |- ( F = G -> ( ( Fun F /\ dom F = A ) <-> ( Fun G /\ dom G = A ) ) )
5		df-fn 5185	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
6		df-fn 5185	. 2 |- ( G Fn A <-> ( Fun G /\ dom G = A ) )
7	4, 5, 6	3bitr4g 222	1 |- ( F = G -> ( F Fn A <-> G Fn A ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1342   dom cdm 4598   Fun wfun 5176   Fn wfn 5177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-in 3117  df-ss 3124  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977  df-opab 4038  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-fun 5184  df-fn 5185

This theorem is referenced by:  fneq1d  5272  fneq1i  5276  fn0  5301  feq1  5314  foeq1  5400  f1ocnv  5439  mpteqb  5570  eufnfv  5709  tfr0dm  6281  tfrlemiex  6290  tfr1onlemsucfn  6299  tfr1onlemsucaccv  6300  tfr1onlembxssdm  6302  tfr1onlembfn  6303  tfr1onlemex  6306  tfr1onlemaccex  6307  tfr1onlemres  6308  mapval2  6635  elixp2  6659  ixpfn  6661  elixpsn  6692  cc2lem  7198  cc3  7200