Theorem fneq2 3575

Description: Equality theorem for function predicate with domain.

Assertion

Ref	Expression
fneq2	|- (A = B -> (F Fn A <-> F Fn B))

Proof of Theorem fneq2

Step	Hyp	Ref	Expression
1		eqeq2 1481	. . 3 |- (A = B -> (dom F = A <-> dom F = B))
2	1	anbi2d 615	. 2 |- (A = B -> ((Fun F /\ dom F = A) <-> (Fun F /\ dom F = B)))
3		df-fn 3188	. 2 |- (F Fn A <-> (Fun F /\ dom F = A))
4		df-fn 3188	. 2 |- (F Fn B <-> (Fun F /\ dom F = B))
5	2, 3, 4	3bitr4g 554	1 |- (A = B -> (F Fn A <-> F Fn B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954  dom cdm 3165  Fun wfun 3171   Fn wfn 3172

This theorem is referenced by:  feq2 3613  feq23 3615  foeq2 3660  f1o00 3705  eqfnfv 3788  fconstfv 3840  tfrlem3 3904  tfrlem12 3913  ixpeq1 4343  aceq3 4713  ac7g 4729  ac5 4732  fodom 4778

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-17 969  ax-4 971  ax-5o 973  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-cleq 1467  df-fn 3188

Copyright terms: Public domain