Theorem fneq2 5277

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 2175	. . 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 5191	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5191	. 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 1343   dom cdm 4604   Fun wfun 5182   Fn wfn 5183

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-cleq 2158  df-fn 5191

This theorem is referenced by:  fneq2d  5279  fneq2i  5283  feq2  5321  foeq2  5407  f1o00  5467  eqfnfv2  5584  tfr0dm  6290  tfrlemisucaccv  6293  tfrlemi1  6300  tfrlemi14d  6301  tfrexlem  6302  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemaccex  6316  tfr1onlemres  6317  ixpeq1  6675  0fz1  9980