Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dff1o3 | Structured version Visualization version GIF version |
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) |
Ref | Expression |
---|---|
dff1o3 | ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3anan32 1093 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) | |
2 | dff1o2 6614 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
3 | df-fo 6355 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | 3 | anbi1i 625 | . 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) |
5 | 1, 2, 4 | 3bitr4i 305 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ◡ccnv 5548 ran crn 5550 Fun wfun 6343 Fn wfn 6344 –onto→wfo 6347 –1-1-onto→wf1o 6348 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-in 3942 df-ss 3951 df-f 6353 df-f1 6354 df-fo 6355 df-f1o 6356 |
This theorem is referenced by: f1ofo 6616 resdif 6629 f1opw 7395 f11o 7642 1stconst 7789 2ndconst 7790 curry1 7793 curry2 7796 f1o2ndf1 7812 ssdomg 8549 phplem4 8693 php3 8697 f1opwfi 8822 cantnfp1lem3 9137 fpwwe2lem6 10051 canthp1lem2 10069 odf1o2 18692 dprdf1o 19148 relogf1o 25144 iseupthf1o 27975 padct 30449 ballotlemfrc 31779 poimirlem1 34887 poimirlem2 34888 poimirlem3 34889 poimirlem4 34890 poimirlem6 34892 poimirlem7 34893 poimirlem9 34895 poimirlem11 34897 poimirlem12 34898 poimirlem13 34899 poimirlem14 34900 poimirlem16 34902 poimirlem17 34903 poimirlem19 34905 poimirlem20 34906 poimirlem23 34909 poimirlem24 34910 poimirlem25 34911 poimirlem29 34915 poimirlem31 34917 ntrneifv2 40423 |
Copyright terms: Public domain | W3C validator |