Theorem fneq2 5679

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

Assertion

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

Proof of Theorem fneq2

Step	Hyp	Ref	Expression
1		eqeq2 2437	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 708	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5600	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5600	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 291	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   <-> wb 187   /\ wa 370   = wceq 1437   dom cdm 4849   Fun wfun 5591   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-ext 2400

This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2414  df-fn 5600

This theorem is referenced by:  fneq2d  5681  fneq2i  5685  feq2  5725  foeq2  5803  f1o00  5859  eqfnfv2  5988  fconstfvOLD  6138  wfrlem1  7039  wfrlem15  7054  tfrlem12  7111  ixpeq1  7537  ac5  8907  0fz1  11819  esumcvgsum  28904  bnj90  29523  bnj919  29573  bnj535  29696  bnj1463  29859  frrlem1  30508  fnchoice  37210