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 1098 | . 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) | |
2 | dff1o2 6623 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
3 | df-fo 6345 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | 3 | anbi1i 627 | . 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) |
5 | 1, 2, 4 | 3bitr4i 306 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 ∧ wa 399 ∧ w3a 1088 = wceq 1542 ◡ccnv 5524 ran crn 5526 Fun wfun 6333 Fn wfn 6334 –onto→wfo 6337 –1-1-onto→wf1o 6338 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-in 3850 df-ss 3860 df-f 6343 df-f1 6344 df-fo 6345 df-f1o 6346 |
This theorem is referenced by: f1ofo 6625 resdif 6638 f1opw 7417 f11o 7673 1stconst 7821 2ndconst 7822 curry1 7825 curry2 7828 f1o2ndf1 7844 ssdomg 8601 phplem4 8749 php3 8753 dif1enlem 8759 f1opwfi 8901 cantnfp1lem3 9216 fpwwe2lem5 10135 canthp1lem2 10153 odf1o2 18816 dprdf1o 19273 relogf1o 25310 iseupthf1o 28139 padct 30629 ballotlemfrc 32063 poimirlem1 35401 poimirlem2 35402 poimirlem3 35403 poimirlem4 35404 poimirlem6 35406 poimirlem7 35407 poimirlem9 35409 poimirlem11 35411 poimirlem12 35412 poimirlem13 35413 poimirlem14 35414 poimirlem16 35416 poimirlem17 35417 poimirlem19 35419 poimirlem20 35420 poimirlem23 35423 poimirlem24 35424 poimirlem25 35425 poimirlem29 35429 poimirlem31 35431 ntrneifv2 41236 |
Copyright terms: Public domain | W3C validator |