Theorem fneq2 5207

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 2147	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 459	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5121	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5121	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 222	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1331   dom cdm 4534   Fun wfun 5112   Fn wfn 5113

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-fn 5121

This theorem is referenced by:  fneq2d  5209  fneq2i  5213  feq2  5251  foeq2  5337  f1o00  5395  eqfnfv2  5512  tfr0dm  6212  tfrlemisucaccv  6215  tfrlemi1  6222  tfrlemi14d  6223  tfrexlem  6224  tfr1onlemsucfn  6230  tfr1onlemsucaccv  6231  tfr1onlembxssdm  6233  tfr1onlembfn  6234  tfr1onlemaccex  6238  tfr1onlemres  6239  ixpeq1  6596  0fz1  9818