Theorem fneq2 5220

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 2150	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 460	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5134	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5134	. 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 1332   dom cdm 4547   Fun wfun 5125   Fn wfn 5126

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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133  df-fn 5134

This theorem is referenced by:  fneq2d  5222  fneq2i  5226  feq2  5264  foeq2  5350  f1o00  5410  eqfnfv2  5527  tfr0dm  6227  tfrlemisucaccv  6230  tfrlemi1  6237  tfrlemi14d  6238  tfrexlem  6239  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemaccex  6253  tfr1onlemres  6254  ixpeq1  6611  0fz1  9856