Theorem feq1 5465

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 5418	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 4959	. . . 4 |- ( F = G -> ran F = ran G )
3	2	sseq1d 3256	. . 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 5330	. 2 |- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )
6		df-f 5330	. 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 1397   C_ wss 3200   ran crn 4726   Fn wfn 5321   -->wf 5322

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-in 3206  df-ss 3213  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089  df-opab 4151  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-fun 5328  df-fn 5329  df-f 5330

This theorem is referenced by:  feq1d  5469  feq1i  5475  f00  5528  f0bi  5529  f0dom0  5530  fconstg  5533  f1eq1  5537  fconst2g  5868  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemex  6525  tfrcllemaccex  6526  tfrcllemres  6527  tfrcl  6529  elmapg  6829  ac6sfi  7086  updjud  7280  finomni  7338  exmidomni  7340  mkvprop  7356  1fv  10373  seqf1oglem2  10781  seqf1og  10782  iswrd  11114  isgrpinv  13636  isghm  13829  upxp  14995  txcn  14998  plyf  15460  griedg0prc  16100  dceqnconst  16664  dcapnconst  16665