Theorem f1eq1 5613

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 5554	. . 3 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )
2		cnveq 5025	. . . 4 |- ( F = G -> `' F = `' G )
3	2	funeqd 5451	. . 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 5435	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
6		df-f1 5435	. 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 1369   `'ccnv 4851   Fun wfun 5424   -->wf 5426   -1-1->wf1 5427

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2736  df-v 2986  df-dif 3343  df-un 3345  df-in 3347  df-ss 3354  df-nul 3650  df-if 3804  df-sn 3890  df-pr 3892  df-op 3896  df-br 4305  df-opab 4363  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-fun 5432  df-fn 5433  df-f 5434  df-f1 5435

This theorem is referenced by:  f1oeq1  5644  f1eq123d  5648  fo00  5686  fun11iun  6549  tposf12  6782  oacomf1olem  7015  f1dom2g  7339  f1domg  7341  dom3d  7363  domtr  7374  domssex2  7483  1sdom  7527  marypha1lem  7695  fseqenlem1  8206  dfac12lem2  8325  dfac12lem3  8326  ackbij2  8424  fin23lem28  8521  fin23lem32  8525  fin23lem34  8527  fin23lem35  8528  fin23lem41  8533  iundom2g  8716  pwfseqlem5  8842  hashf1lem1  12220  hashf1lem2  12221  hashf1  12222  4sqlem11  14028  conjsubgen  15791  sylow1lem2  16110  sylow2blem1  16131  hauspwpwf1  19572  axlowdim  23219  isuslgra  23283  isusgra  23284  usgrares  23300  sizeusglecusg  23406  2trllemE  23464  constr1trl  23499  specval  25314  zrhchr  26417  qqhre  26458  eldioph2lem2  29111