Theorem fneq2 5324

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 2199	. . 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 5238	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5238	. 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 4644   Fun wfun 5229   Fn wfn 5230

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 2171

This theorem depends on definitions:  df-bi 117  df-cleq 2182  df-fn 5238

This theorem is referenced by:  fneq2d  5326  fneq2i  5330  feq2  5368  foeq2  5454  f1o00  5515  eqfnfv2  5635  tfr0dm  6347  tfrlemisucaccv  6350  tfrlemi1  6357  tfrlemi14d  6358  tfrexlem  6359  tfr1onlemsucfn  6365  tfr1onlemsucaccv  6366  tfr1onlembxssdm  6368  tfr1onlembfn  6369  tfr1onlemaccex  6373  tfr1onlemres  6374  ixpeq1  6735  0fz1  10075