Theorem fneq2d 4506

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 4504	. 2 |- (A = B -> (F Fn A <-> F Fn B))
3	1, 2	syl 12	1 |- (ph -> (F Fn A <-> F Fn B))

Syntax hints:   -> wi 3   <-> wb 163   = wceq 1298   Fn wfn 3993

This theorem is referenced by:  aceq3 5895  ac7g 5911  fodom 5960  bnj148 12481  bnj927 12835  bnj1470 13147  fneq2dOLD 13585  fneq12d 13586  unprj 14511  cnpfillim 15589  sdclem1 15809  dfstruct2 16709  fnelstr 16717  strdif 16719

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877  df-fn 4009

Copyright terms: Public domain