Theorem fneq2 5307

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 2187	. . 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 5221	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
4		df-fn 5221	. 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 1353   dom cdm 4628   Fun wfun 5212   Fn wfn 5213

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-cleq 2170  df-fn 5221

This theorem is referenced by:  fneq2d  5309  fneq2i  5313  feq2  5351  foeq2  5437  f1o00  5498  eqfnfv2  5616  tfr0dm  6325  tfrlemisucaccv  6328  tfrlemi1  6335  tfrlemi14d  6336  tfrexlem  6337  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlembfn  6347  tfr1onlemaccex  6351  tfr1onlemres  6352  ixpeq1  6711  0fz1  10047