Theorem fneq2d 5467

Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq2d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
fneq2d	|- ( ph -> ( F Fn A <-> F Fn B ) )

Proof of Theorem fneq2d

Step	Hyp	Ref	Expression
1		fneq2d.1	. 2 |- ( ph -> A = B )
2		fneq2 5465	. 2 |- ( A = B -> ( F Fn A <-> F Fn B ) )
3	1, 2	syl 14	1 |- ( ph -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   <-> wb 105   = wceq 1402   Fn wfn 5367

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231  df-fn 5375

This theorem is referenced by:  fneq12d  5468  fncofn  5884  acfun  7553  ccfunen  7620  ccatlid  11352  ccatrid  11353  ccatass  11354  ccatswrd  11420  swrdccat2  11421  ccatpfx  11451  swrdswrd  11455  swrdccatin2  11479  pfxccatin12  11483  seq3shft  11581  ptex  13595  rng1zrlem  14233