Theorem f1eq1 5796

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 5731	. . 3 |- ( F = G -> ( F : A --> B <-> G : A --> B ) )
2		cnveq 5026	. . . 4 |- ( F = G -> `' F = `' G )
3	2	funeqd 5621	. . 3 |- ( F = G -> ( Fun `' F <-> Fun `' G ) )
4	1, 3	anbi12d 722	. 2 |- ( F = G -> ( ( F : A --> B /\ Fun `' F ) <-> ( G : A --> B /\ Fun `' G ) ) )
5		df-f1 5605	. 2 |- ( F : A -1-1-> B <-> ( F : A --> B /\ Fun `' F ) )
6		df-f1 5605	. 2 |- ( G : A -1-1-> B <-> ( G : A --> B /\ Fun `' G ) )
7	4, 5, 6	3bitr4g 296	1 |- ( F = G -> ( F : A -1-1-> B <-> G : A -1-1-> B ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1454   `'ccnv 4851   Fun wfun 5594   -->wf 5596   -1-1->wf1 5597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-rab 2757  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-br 4416  df-opab 4475  df-rel 4859  df-cnv 4860  df-co 4861  df-dm 4862  df-rn 4863  df-fun 5602  df-fn 5603  df-f 5604  df-f1 5605

This theorem is referenced by:  f1oeq1  5827  f1eq123d  5831  fo00  5870  f1prex  6206  fun11iun  6779  tposf12  7023  oacomf1olem  7290  f1dom2g  7612  f1domg  7614  dom3d  7636  domtr  7647  domssex2  7757  1sdom  7800  marypha1lem  7972  fseqenlem1  8480  dfac12lem2  8599  dfac12lem3  8600  ackbij2  8698  fin23lem28  8795  fin23lem32  8799  fin23lem34  8801  fin23lem35  8802  fin23lem41  8807  iundom2g  8990  pwfseqlem5  9113  hashf1lem1  12650  hashf1lem2  12651  hashf1  12652  4sqlem11  14947  conjsubgen  16963  sylow1lem2  17299  sylow2blem1  17320  hauspwpwf1  21050  istrkg2ld  24556  axlowdim  25039  isuslgra  25118  isusgra  25119  usgrares  25144  sizeusglecusg  25262  2trllemE  25331  constr1trl  25366  specval  27599  aciunf1lem  28312  zrhchr  28828  qqhre  28872  eldioph2lem2  35647  meadjiunlem  38340  sizusglecusg  39573