Theorem f1eq1 5593

Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)

Assertion

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

Proof of Theorem f1eq1

Step	Hyp	Ref	Expression
1		feq1 5535	. . 3 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )
2		cnveq 5005	. . . 4 |- ( F = G -> `' F = `' G )
3	2	funeqd 5434	. . 3 |- ( F = G -> ( Fun `' F <-> Fun `' G ) )
4	1, 3	anbi12d 692	. 2 |- ( F = G -> ( ( F : A --> B /\ Fun `' F ) <-> ( G : A --> B /\ Fun `' G ) ) )
5		df-f1 5418	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
6		df-f1 5418	. 2 |- ( G : A -1-1-> B <-> ( G : A --> B /\ Fun `' G ) )
7	4, 5, 6	3bitr4g 280	1 |- ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   `'ccnv 4836   Fun wfun 5407   -->wf 5409   -1-1->wf1 5410

This theorem is referenced by:  f1oeq1  5624  f1eq123d  5628  fun11iun  5654  fo00  5670  tposf12  6463  oacomf1olem  6766  f1dom2g  7084  f1domg  7086  dom3d  7108  domtr  7119  domssex2  7226  1sdom  7270  marypha1lem  7396  fseqenlem1  7861  dfac12lem2  7980  dfac12lem3  7981  ackbij2  8079  fin23lem28  8176  fin23lem32  8180  fin23lem34  8182  fin23lem35  8183  fin23lem41  8188  iundom2g  8371  pwfseqlem5  8494  hashf1lem1  11659  hashf1lem2  11660  hashf1  11661  4sqlem11  13278  conjsubgen  14993  sylow1lem2  15188  sylow2blem1  15209  hauspwpwf1  17972  isuslgra  21325  isusgra  21326  usgrares  21342  sizeusglecusg  21448  2trllemE  21506  constr1trl  21541  specval  23354  zrhchr  24313  qqhre  24339  axlowdim  25804  eldioph2lem2  26709

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-br 4173  df-opab 4227  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418