Theorem f1eq1 5775

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 5712	. . 3 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )
2		cnveq 5175	. . . 4 |- ( F = G -> `' F = `' G )
3	2	funeqd 5608	. . 3 |- ( F = G -> ( Fun `' F <-> Fun `' G ) )
4	1, 3	anbi12d 710	. 2 |- ( F = G -> ( ( F : A --> B /\ Fun `' F ) <-> ( G : A --> B /\ Fun `' G ) ) )
5		df-f1 5592	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
6		df-f1 5592	. 2 |- ( G : A -1-1-> B <-> ( G : A --> B /\ Fun `' G ) )
7	4, 5, 6	3bitr4g 288	1 |- ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   `'ccnv 4998   Fun wfun 5581   -->wf 5583   -1-1->wf1 5584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448  df-opab 4506  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592

This theorem is referenced by:  f1oeq1  5806  f1eq123d  5810  fo00  5848  fun11iun  6744  tposf12  6980  oacomf1olem  7213  f1dom2g  7533  f1domg  7535  dom3d  7557  domtr  7568  domssex2  7677  1sdom  7722  marypha1lem  7892  fseqenlem1  8404  dfac12lem2  8523  dfac12lem3  8524  ackbij2  8622  fin23lem28  8719  fin23lem32  8723  fin23lem34  8725  fin23lem35  8726  fin23lem41  8731  iundom2g  8914  pwfseqlem5  9040  hashf1lem1  12469  hashf1lem2  12470  hashf1  12471  4sqlem11  14331  conjsubgen  16101  sylow1lem2  16422  sylow2blem1  16443  hauspwpwf1  20239  istrkg2ld  23602  axlowdim  23956  isuslgra  24035  isusgra  24036  usgrares  24061  sizeusglecusg  24178  2trllemE  24247  constr1trl  24282  specval  26509  zrhchr  27609  qqhre  27650  eldioph2lem2  30314