![]() |
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 6790 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵)) | |
3 | df-fo 6503 | . . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵)) | |
4 | 3 | anbi1i 625 | . 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹)) |
5 | 1, 2, 4 | 3bitr4i 303 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ◡ccnv 5633 ran crn 5635 Fun wfun 6491 Fn wfn 6492 –onto→wfo 6495 –1-1-onto→wf1o 6496 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-3an 1090 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-v 3448 df-in 3918 df-ss 3928 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 |
This theorem is referenced by: f1ofo 6792 resdif 6806 f1opw 7610 f11o 7880 1stconst 8033 2ndconst 8034 curry1 8037 curry2 8040 f1o2ndf1 8055 ssdomg 8941 dif1enlem 9101 dif1enlemOLD 9102 phplem2 9153 php3 9157 phplem4OLD 9165 php3OLD 9169 f1opwfi 9301 cantnfp1lem3 9617 fpwwe2lem5 10572 canthp1lem2 10590 odf1o2 19356 dprdf1o 19812 relogf1o 25925 iseupthf1o 29149 padct 31639 ballotlemfrc 33129 poimirlem1 36082 poimirlem2 36083 poimirlem3 36084 poimirlem4 36085 poimirlem6 36087 poimirlem7 36088 poimirlem9 36090 poimirlem11 36092 poimirlem12 36093 poimirlem13 36094 poimirlem14 36095 poimirlem16 36097 poimirlem17 36098 poimirlem19 36100 poimirlem20 36101 poimirlem23 36104 poimirlem24 36105 poimirlem25 36106 poimirlem29 36110 poimirlem31 36112 ntrneifv2 42359 |
Copyright terms: Public domain | W3C validator |