Theorem fneq2 5212

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 2149	. . 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 5126	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5126	. 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 4539   Fun wfun 5117   Fn wfn 5118

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 2121

This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-fn 5126

This theorem is referenced by:  fneq2d  5214  fneq2i  5218  feq2  5256  foeq2  5342  f1o00  5402  eqfnfv2  5519  tfr0dm  6219  tfrlemisucaccv  6222  tfrlemi1  6229  tfrlemi14d  6230  tfrexlem  6231  tfr1onlemsucfn  6237  tfr1onlemsucaccv  6238  tfr1onlembxssdm  6240  tfr1onlembfn  6241  tfr1onlemaccex  6245  tfr1onlemres  6246  ixpeq1  6603  0fz1  9825