Theorem fneq2 3583

Description: Equality theorem for function predicate with domain.

Assertion

Ref	Expression
fneq2	|- (A = B -> (F Fn A <-> F Fn B))

Proof of Theorem fneq2

Step	Hyp	Ref	Expression
1		eqeq2 1484	. . 3 |- (A = B -> (dom F = A <-> dom F = B))
2	1	anbi2d 616	. 2 |- (A = B -> ((Fun F /\ dom F = A) <-> (Fun F /\ dom F = B)))
3		df-fn 3193	. 2 |- (F Fn A <-> (Fun F /\ dom F = A))
4		df-fn 3193	. 2 |- (F Fn B <-> (Fun F /\ dom F = B))
5	2, 3, 4	3bitr4g 555	1 |- (A = B -> (F Fn A <-> F Fn B))

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

This theorem is referenced by:  feq2 3621  feq23 3623  foeq2 3669  f1o00 3714  eqfnfv 3797  fconstfv 3849  tfrlem3 3913  tfrlem12 3922  ixpeq1 4353  aceq3 4733  ac7g 4749  ac5 4752  fodom 4798

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-17 971  ax-4 973  ax-5o 975  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1469  df-fn 3193

Copyright terms: Public domain