Theorem fneq2 5039

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 2092	. . 3 |- ( A = B -> ( dom F = A <-> dom F = B ) )
2	1	anbi2d 452	. 2 |- ( A = B -> ( ( Fun F /\ dom F = A ) <-> ( Fun F /\ dom F = B ) ) )
3		df-fn 4955	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 4955	. 2 |- ( F Fn B <-> ( Fun F /\ dom F = B ) )
5	2, 3, 4	3bitr4g 221	1 |- ( A = B -> ( F Fn A <-> F Fn B ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1285   dom cdm 4391   Fun wfun 4946   Fn wfn 4947

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076  df-fn 4955

This theorem is referenced by:  fneq2d  5041  fneq2i  5045  feq2  5082  foeq2  5154  f1o00  5212  eqfnfv2  5318  tfr0dm  5991  tfrlemisucaccv  5994  tfrlemi1  6001  tfrlemi14d  6002  tfrexlem  6003  tfr1onlemsucfn  6009  tfr1onlemsucaccv  6010  tfr1onlembxssdm  6012  tfr1onlembfn  6013  tfr1onlemaccex  6017  tfr1onlemres  6018  0fz1  9192