Theorem fneq2 5980

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 2633	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 740	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5891	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5891	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 303	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   dom cdm 5114   Fun wfun 5882   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fn 5891

This theorem is referenced by:  fneq2d  5982  fneq2i  5986  feq2  6027  foeq2  6112  f1o00  6171  eqfnfv2  6312  wfrlem1  7414  wfrlem15  7429  tfrlem12  7485  ixpeq1  7919  ac5  9299  0fz1  12361  esumcvgsum  30150  bnj90  30788  bnj919  30837  bnj535  30960  bnj1463  31123  frrlem1  31780  fnchoice  39188