Theorem fneq2 5611

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 2469	. . 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 5532	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5532	. 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 1370   dom cdm 4951   Fun wfun 5523   Fn wfn 5524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446  df-fn 5532

This theorem is referenced by:  fneq2d  5613  fneq2i  5617  feq2  5654  foeq2  5728  f1o00  5784  eqfnfv2  5910  fconstfv  6052  tfrlem12  6961  ixpeq1  7387  ac5  8760  0fz1  11589  wfrlem1  27888  wfrlem15  27902  frrlem1  27932  fnchoice  29919  bnj90  32063  bnj919  32112  bnj535  32235  bnj1463  32398