Theorem fneq2 5676

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 2482	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 703	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5597	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5597	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 288	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   dom cdm 5005   Fun wfun 5588   Fn wfn 5589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5597

This theorem is referenced by:  fneq2d  5678  fneq2i  5682  feq2  5720  foeq2  5798  f1o00  5854  eqfnfv2  5983  fconstfv  6134  tfrlem12  7070  ixpeq1  7492  ac5  8869  0fz1  11717  wfrlem1  29261  wfrlem15  29275  frrlem1  29305  fnchoice  31297  bnj90  33211  bnj919  33260  bnj535  33383  bnj1463  33546