![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1eq1 | Structured version Visualization version GIF version |
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.) |
Ref | Expression |
---|---|
f1eq1 | ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | feq1 6704 | . . 3 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵)) | |
2 | cnveq 5876 | . . . 4 ⊢ (𝐹 = 𝐺 → ◡𝐹 = ◡𝐺) | |
3 | 2 | funeqd 6576 | . . 3 ⊢ (𝐹 = 𝐺 → (Fun ◡𝐹 ↔ Fun ◡𝐺)) |
4 | 1, 3 | anbi12d 630 | . 2 ⊢ (𝐹 = 𝐺 → ((𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹) ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺))) |
5 | df-f1 6554 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹)) | |
6 | df-f1 6554 | . 2 ⊢ (𝐺:𝐴–1-1→𝐵 ↔ (𝐺:𝐴⟶𝐵 ∧ Fun ◡𝐺)) | |
7 | 4, 5, 6 | 3bitr4g 313 | 1 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴–1-1→𝐵 ↔ 𝐺:𝐴–1-1→𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ◡ccnv 5677 Fun wfun 6543 ⟶wf 6545 –1-1→wf1 6546 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-br 5150 df-opab 5212 df-rel 5685 df-cnv 5686 df-co 5687 df-dm 5688 df-rn 5689 df-fun 6551 df-fn 6552 df-f 6553 df-f1 6554 |
This theorem is referenced by: f1oeq1 6826 f1eq123d 6830 fo00 6874 f1prex 7293 f1iun 7948 tposf12 8257 oacomf1olem 8585 f1dom4g 8986 f1dom3g 8988 f1dom2gOLD 8991 f1domg 8993 dom3d 9015 domtr 9028 0domg 9125 domssex2 9162 1sdomOLD 9274 marypha1lem 9458 fseqenlem1 10049 dfac12lem2 10169 dfac12lem3 10170 ackbij2 10268 fin23lem28 10365 fin23lem32 10369 fin23lem34 10371 fin23lem35 10372 fin23lem41 10377 iundom2g 10565 pwfseqlem5 10688 hashf1lem1 14451 hashf1lem1OLD 14452 hashf1lem2 14453 hashf1 14454 4sqlem11 16927 injsubmefmnd 18857 conjsubgen 19214 sylow1lem2 19566 sylow2blem1 19587 hauspwpwf1 23935 istrkg2ld 28336 axlowdim 28844 sizusglecusg 29349 specval 31780 aciunf1lem 32529 zrhchr 33708 qqhre 33752 hashnexinj 41731 eldioph2lem2 42323 meadjiunlem 45991 fcoresf1b 46590 fundcmpsurbijinjpreimafv 46884 fundcmpsurinjpreimafv 46885 fundcmpsurinjimaid 46888 f1sn2g 48089 f102g 48090 |
Copyright terms: Public domain | W3C validator |