f1oeq2 - Metamath Proof Explorer

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

Theorem f1oeq2 6041

Description: Equality theorem for one-to-one onto functions. (Contributed by NM, 10-Feb-1997.)

**Assertion**
Ref	Expression
f1oeq2	⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

**Proof of Theorem f1oeq2**
Step	Hyp	Ref	Expression
1		f1eq2 6010	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6025	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 743	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 5811	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 5811	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 302	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 –1-1→wf1 5801 –onto→wfo 5802 –1-1-onto→wf1o 5803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590

This theorem depends on definitions: df-bi 196 df-an 385 df-cleq 2603 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811

This theorem is referenced by: f1oeq23 6043 f1oeq123d 6046 resin 6071 f1osng 6089 f1o2sn 6314 fveqf1o 6457 isoeq4 6470 oacomf1o 7532 bren 7850 f1dmvrnfibi 8133 marypha1lem 8222 oef1o 8478 cnfcomlem 8479 cnfcom 8480 cnfcom2 8482 infxpenc 8724 infxpenc2 8728 pwfseqlem5 9364 pwfseq 9365 summolem3 14292 summo 14295 fsum 14298 fsumf1o 14301 sumsn 14319 prodmolem3 14502 prodmo 14505 fprod 14510 fprodf1o 14515 prodsn 14531 prodsnf 14533 gsumvalx 17093 gsumpropd 17095 gsumpropd2lem 17096 gsumval3lem1 18129 gsumval3 18131 znhash 19726 znunithash 19732 imasf1oxms 22104 cncfcnvcn 22532 wlknwwlknvbij 26268 clwwlkvbij 26329 eupai 26494 eupatrl 26495 eupa0 26501 eupares 26502 eupap1 26503 f1ocnt 28946 derangval 30403 subfacp1lem2a 30416 subfacp1lem3 30418 subfacp1lem5 30420 erdsze2lem1 30439 ismtyval 32769 rngoisoval 32946 lautset 34386 pautsetN 34402 eldioph2lem1 36341 imasgim 36688 sumsnd 38208 f1oeq2d 38356 sumsnf 38636 stoweidlem35 38928 stoweidlem39 38932 wlksnwwlknvbij 41114 clwwlksvbij 41229 eupthp1 41384