Theorem fneq1 3582

Description: Equality theorem for function predicate with domain.

Assertion

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

Proof of Theorem fneq1

Step	Hyp	Ref	Expression
1		funeq 3535	. . 3 |- (F = G -> (Fun F <-> Fun G))
2		dmeq 3311	. . . 4 |- (F = G -> dom F = dom G)
3	2	eqeq1d 1483	. . 3 |- (F = G -> (dom F = A <-> dom G = A))
4	1, 3	anbi12d 628	. 2 |- (F = G -> ((Fun F /\ dom F = A) <-> (Fun G /\ dom G = A)))
5		df-fn 3193	. 2 |- (F Fn A <-> (Fun F /\ dom F = A))
6		df-fn 3193	. 2 |- (G Fn A <-> (Fun G /\ dom G = A))
7	4, 5, 6	3bitr4g 555	1 |- (F = G -> (F Fn A <-> G Fn A))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956  dom cdm 3170  Fun wfun 3176   Fn wfn 3177

This theorem is referenced by:  fn0 3605  fnopabg 3615  feq1 3620  foeq1 3668  f1oun 3706  f1o00 3714  f1osn 3719  fnopabfv 3758  tfrlem3 3913  tfrlem10 3920  tfrlem12 3922  abianfp 3962  curry1 4098  mapval2 4335  elixp2 4349  en2d 4400  pw2en 4446  mapxpen 4495  unblem4 4543  inf3lem6 4618  r1fnon 4650  aceq3lem 4732  aceq4 4734  alephfnon 4862  alephfplem4 4899  alephfp 4900  om2uzran 6300  om2uzf1o 6301  shftfn 6343  seqzfn 6539  seq0fn 6546  dfseq0 6563  neif 7715  grpinvf 8079  ghgrpilem4 8136  0vfval 8225

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620  df-opab 2667  df-id 2835  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-fun 3192  df-fn 3193

Copyright terms: Public domain