Theorem fneq2 5364

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 2215	. . 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 5275	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5275	. 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 1373   dom cdm 4676   Fun wfun 5266   Fn wfn 5267

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-fn 5275

This theorem is referenced by:  fneq2d  5366  fneq2i  5370  feq2  5411  foeq2  5497  f1o00  5559  eqfnfv2  5680  tfr0dm  6410  tfrlemisucaccv  6413  tfrlemi1  6420  tfrlemi14d  6421  tfrexlem  6422  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemaccex  6436  tfr1onlemres  6437  ixpeq1  6798  0fz1  10169