Theorem feq1 5348

Description: Equality theorem for functions. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
feq1	|- ( F = G -> ( F : A --> B <-> G : A --> B ) )

Proof of Theorem feq1

Step	Hyp	Ref	Expression
1		fneq1 5304	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 4854	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3184	. . 3 |- ( F = G -> ( ran F C_ B <-> ran G C_ B ) )
4	1, 3	anbi12d 473	. 2 |- ( F = G -> ( ( F Fn A /\ ran F C_ B ) <-> ( G Fn A /\ ran G C_ B ) ) )
5		df-f 5220	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5220	. 2 |- ( G : A --> B <-> ( G Fn A /\ ran G C_ B ) )
7	4, 5, 6	3bitr4g 223	1 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   C_ wss 3129   ran crn 4627   Fn wfn 5211   -->wf 5212

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-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-br 4004  df-opab 4065  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-fun 5218  df-fn 5219  df-f 5220

This theorem is referenced by:  feq1d  5352  feq1i  5358  f00  5407  f0bi  5408  f0dom0  5409  fconstg  5412  f1eq1  5416  fconst2g  5731  tfrcllemsucfn  6353  tfrcllemsucaccv  6354  tfrcllembxssdm  6356  tfrcllembfn  6357  tfrcllemex  6360  tfrcllemaccex  6361  tfrcllemres  6362  tfrcl  6364  elmapg  6660  ac6sfi  6897  updjud  7080  finomni  7137  exmidomni  7139  mkvprop  7155  1fv  10138  isgrpinv  12925  upxp  13708  txcn  13711  dceqnconst  14743  dcapnconst  14744