f1oen - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > f1oen		Structured version Visualization version GIF version

Theorem f1oen 8992

Description: The domain and range of a one-to-one, onto function are equinumerous. (Contributed by NM, 19-Jun-1998.)

**Hypothesis**
Ref	Expression
f1oen.1	⊢ 𝐴 ∈ V

**Assertion**
Ref	Expression
f1oen	⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐴 ≈ 𝐵)

**Proof of Theorem f1oen**
Step	Hyp	Ref	Expression
1		f1oen.1	. 2 ⊢ 𝐴 ∈ V
2		f1oeng 8990	. 2 ⊢ ((𝐴 ∈ V ∧ 𝐹:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵)
3	1, 2	mpan 688	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐴 ≈ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∈ wcel 2098 Vcvv 3463 class class class wbr 5148 –1-1-onto→wf1o 6546 ≈ cen 8959

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-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739

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-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3775 df-csb 3891 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6499 df-fun 6549 df-fn 6550 df-f 6551 df-f1 6552 df-fo 6553 df-f1o 6554 df-fv 6555 df-en 8963

This theorem is referenced by: mapfien2 9432 infxpenlem 10036 dfac8alem 10052 dfac12lem2 10167 dfac12lem3 10168 r1om 10267 axcc2lem 10459 summolem3 15693 summolem2 15695 zsum 15697 prodmolem3 15910 prodmolem2 15912 zprod 15914 cpnnen 16206 eulerthlem2 16751 hashgcdeq 16758 4sqlem11 16924 gicen 19237 odhash 19534 odhash2 19535 sylow1lem2 19559 sylow2blem1 19580 znhash 21497 wlkswwlksen 29748 wlknwwlksnen 29757 eupthfi 30072 numclwwlk1lem2 30227 ballotlemfrc 34233 ballotlem8 34243 erdszelem10 34897 poimirlem4 37184 poimirlem26 37206 poimirlem27 37207 pwfi2en 42603 gricen 47319 aacllem 48362

	
		OSZAR »