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 6290

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 6258	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6274	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 749	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 6056	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 6056	. 2 ⊢ (𝐹:𝐵–1-1-onto→𝐶 ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶))
6	3, 4, 5	3bitr4g 303	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1-onto→𝐶 ↔ 𝐹:𝐵–1-1-onto→𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1632 –1-1→wf1 6046 –onto→wfo 6047 –1-1-onto→wf1o 6048

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740

This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 df-fn 6052 df-f 6053 df-f1 6054 df-fo 6055 df-f1o 6056

This theorem is referenced by: f1oeq23 6292 f1oeq123d 6295 resin 6320 f1osng 6339 f1o2sn 6572 fveqf1o 6721 isoeq4 6734 oacomf1o 7816 bren 8132 f1dmvrnfibi 8417 marypha1lem 8506 oef1o 8770 cnfcomlem 8771 cnfcom 8772 cnfcom2 8774 infxpenc 9051 infxpenc2 9055 pwfseqlem5 9697 pwfseq 9698 summolem3 14664 summo 14667 fsum 14670 fsumf1o 14673 sumsnf 14692 sumsn 14694 prodmolem3 14882 prodmo 14885 fprod 14890 fprodf1o 14895 prodsn 14911 prodsnf 14913 gsumvalx 17491 gsumpropd 17493 gsumpropd2lem 17494 gsumval3lem1 18526 gsumval3 18528 znhash 20129 znunithash 20135 imasf1oxms 22515 cncfcnvcn 22945 wlksnwwlknvbij 27047 clwwlkvbij 27283 clwwlkvbijOLD 27284 eupthp1 27389 f1ocnt 29889 derangval 31477 subfacp1lem2a 31490 subfacp1lem3 31492 subfacp1lem5 31494 erdsze2lem1 31513 ismtyval 33930 rngoisoval 34107 lautset 35889 pautsetN 35905 eldioph2lem1 37843 imasgim 38190 sumsnd 39702 f1oeq2d 39878 stoweidlem35 40773 stoweidlem39 40777 uspgrsprfo 42284