Theorem fneq2 5344

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 2203	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 464	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5258	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5258	. 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 1364   dom cdm 4660   Fun wfun 5249   Fn wfn 5250

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-fn 5258

This theorem is referenced by:  fneq2d  5346  fneq2i  5350  feq2  5388  foeq2  5474  f1o00  5536  eqfnfv2  5657  tfr0dm  6377  tfrlemisucaccv  6380  tfrlemi1  6387  tfrlemi14d  6388  tfrexlem  6389  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemaccex  6403  tfr1onlemres  6404  ixpeq1  6765  0fz1  10114