Theorem fneq2 5382

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 2217	. . 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 5293	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5293	. 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 4693   Fun wfun 5284   Fn wfn 5285

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200  df-fn 5293

This theorem is referenced by:  fneq2d  5384  fneq2i  5388  feq2  5429  foeq2  5517  f1o00  5580  eqfnfv2  5701  tfr0dm  6431  tfrlemisucaccv  6434  tfrlemi1  6441  tfrlemi14d  6442  tfrexlem  6443  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemaccex  6457  tfr1onlemres  6458  ixpeq1  6819  0fz1  10202