Theorem fneq2 5465

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 2248	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 468	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5375	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5375	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   dom cdm 4769   Fun wfun 5366   Fn wfn 5367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5375

This theorem is referenced by:  fneq2d  5467  fneq2i  5471  feq2  5512  foeq2  5607  f1o00  5671  eqfnfv2  5798  tfr0dm  6583  tfrlemisucaccv  6586  tfrlemi1  6593  tfrlemi14d  6594  tfrexlem  6595  tfr1onlemsucfn  6601  tfr1onlemsucaccv  6602  tfr1onlembxssdm  6604  tfr1onlembfn  6605  tfr1onlemaccex  6609  tfr1onlemres  6610  ixpeq1  6981  0fz1  10428