Theorem fneq2 5343

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 2203	. . 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 5257	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5257	. 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 4659   Fun wfun 5248   Fn wfn 5249

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-cleq 2186  df-fn 5257

This theorem is referenced by:  fneq2d  5345  fneq2i  5349  feq2  5387  foeq2  5473  f1o00  5535  eqfnfv2  5656  tfr0dm  6375  tfrlemisucaccv  6378  tfrlemi1  6385  tfrlemi14d  6386  tfrexlem  6387  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemaccex  6401  tfr1onlemres  6402  ixpeq1  6763  0fz1  10111