Theorem foeq1 5496

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

Assertion

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

Proof of Theorem foeq1

Step	Hyp	Ref	Expression
1		fneq1 5363	. . 3 |- ( F = G -> ( F Fn A <-> G Fn A ) )
2		rneq 4906	. . . 4 |- ( F = G -> ran F = ran G )
3	2	eqeq1d 2214	. . 3 |- ( F = G -> ( ran F = B <-> ran G = B ) )
4	1, 3	anbi12d 473	. 2 |- ( F = G -> ( ( F Fn A /\ ran F = B ) <-> ( G Fn A /\ ran G = B ) ) )
5		df-fo 5278	. 2 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
6		df-fo 5278	. 2 |- ( G : A -onto-> B <-> ( G Fn A /\ ran G = B ) )
7	4, 5, 6	3bitr4g 223	1 |- ( F = G -> ( F : A -onto-> B <-> G : A -onto-> B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1373   ran crn 4677   Fn wfn 5267   -onto->wfo 5270

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-in 3172  df-ss 3179  df-sn 3639  df-pr 3640  df-op 3642  df-br 4046  df-opab 4107  df-rel 4683  df-cnv 4684  df-co 4685  df-dm 4686  df-rn 4687  df-fun 5274  df-fn 5275  df-fo 5278

This theorem is referenced by:  f1oeq1  5512  foeq123d  5517  resdif  5546  dif1en  6978  0ct  7211  ctmlemr  7212  ctm  7213  ctssdclemn0  7214  ctssdclemr  7216  ctssdc  7217  enumct  7219  omct  7221  ctssexmid  7254  exmidfodomrlemim  7311  nninfct  12395  ennnfonelemim  12828  ctinfomlemom  12831  ctinfom  12832  ctinf  12834  qnnen  12835  enctlem  12836  ctiunct  12844  omctfn  12847  ssomct  12849  mndfo  13304  znzrhfo  14443  subctctexmid  15974  domomsubct  15975