Theorem fneq2 5287

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 2180	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 461	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 5201	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5201	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 222	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1348   dom cdm 4611   Fun wfun 5192   Fn wfn 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-fn 5201

This theorem is referenced by:  fneq2d  5289  fneq2i  5293  feq2  5331  foeq2  5417  f1o00  5477  eqfnfv2  5594  tfr0dm  6301  tfrlemisucaccv  6304  tfrlemi1  6311  tfrlemi14d  6312  tfrexlem  6313  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  ixpeq1  6687  0fz1  10001