![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1eq1 | Structured version Visualization version Unicode version |
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1eq1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq1 5731 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | cnveq 5026 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | funeqd 5621 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | anbi12d 722 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | df-f1 5605 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
6 | df-f1 5605 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 4, 5, 6 | 3bitr4g 296 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
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 |
Copyright terms: Public domain | W3C validator |