![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1oen | Structured version Visualization version GIF version |
Description: The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.) |
Ref | Expression |
---|---|
f1oen.1 | ⊢ 𝐴 ∈ V |
Ref | Expression |
---|---|
f1oen | ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐴 ≈ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oen.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | f1oeng 8321 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) | |
3 | 1, 2 | mpan 677 | 1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐴 ≈ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2048 Vcvv 3412 class class class wbr 4927 –1-1-onto→wf1o 6185 ≈ cen 8299 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2747 ax-rep 5047 ax-sep 5058 ax-nul 5065 ax-pow 5117 ax-pr 5184 ax-un 7277 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ne 2965 df-ral 3090 df-rex 3091 df-reu 3092 df-rab 3094 df-v 3414 df-sbc 3681 df-csb 3786 df-dif 3831 df-un 3833 df-in 3835 df-ss 3842 df-nul 4178 df-if 4349 df-pw 4422 df-sn 4440 df-pr 4442 df-op 4446 df-uni 4711 df-iun 4792 df-br 4928 df-opab 4990 df-mpt 5007 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-rn 5415 df-res 5416 df-ima 5417 df-iota 6150 df-fun 6188 df-fn 6189 df-f 6190 df-f1 6191 df-fo 6192 df-f1o 6193 df-fv 6194 df-en 8303 |
This theorem is referenced by: mapfien2 8663 infxpenlem 9229 dfac8alem 9245 dfac12lem2 9360 dfac12lem3 9361 r1om 9460 axcc2lem 9652 summolem3 14925 summolem2 14927 zsum 14929 prodmolem3 15141 prodmolem2 15143 zprod 15145 cpnnen 15436 eulerthlem2 15969 hashgcdeq 15976 4sqlem11 16141 gicen 18182 odhash 18454 odhash2 18455 sylow1lem2 18479 sylow2blem1 18500 znhash 20401 wlkswwlksen 27360 wlknwwlksnen 27370 eupthfi 27728 numclwwlk1lem2 27901 numclwwlk1lem2OLD 27902 ballotlemfrc 31421 ballotlem8 31431 erdszelem10 32022 poimirlem4 34315 poimirlem26 34337 poimirlem27 34338 pwfi2en 39071 aacllem 44243 |
Copyright terms: Public domain | W3C validator |