Theorem fneq2 5348

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 2206	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 464	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5262	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5262	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 223	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1364   dom cdm 4664   Fun wfun 5253   Fn wfn 5254

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-fn 5262

This theorem is referenced by:  fneq2d  5350  fneq2i  5354  feq2  5394  foeq2  5480  f1o00  5542  eqfnfv2  5663  tfr0dm  6389  tfrlemisucaccv  6392  tfrlemi1  6399  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemaccex  6415  tfr1onlemres  6416  ixpeq1  6777  0fz1  10137