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 6085

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 6054	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–1-1→𝐶 ↔ 𝐹:𝐵–1-1→𝐶))
2		foeq2 6069	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴–onto→𝐶 ↔ 𝐹:𝐵–onto→𝐶))
3	1, 2	anbi12d 746	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶) ↔ (𝐹:𝐵–1-1→𝐶 ∧ 𝐹:𝐵–onto→𝐶)))
4		df-f1o 5854	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐶 ↔ (𝐹:𝐴–1-1→𝐶 ∧ 𝐹:𝐴–onto→𝐶))
5		df-f1o 5854	. 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 384 = wceq 1480 –1-1→wf1 5844 –onto→wfo 5845 –1-1-onto→wf1o 5846

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1719 ax-4 1734 ax-5 1836 ax-6 1885 ax-7 1932 ax-9 1996 ax-ext 2601

This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1702 df-cleq 2614 df-fn 5850 df-f 5851 df-f1 5852 df-fo 5853 df-f1o 5854

This theorem is referenced by: f1oeq23 6087 f1oeq123d 6090 resin 6115 f1osng 6134 f1o2sn 6362 fveqf1o 6511 isoeq4 6524 oacomf1o 7590 bren 7908 f1dmvrnfibi 8194 marypha1lem 8283 oef1o 8539 cnfcomlem 8540 cnfcom 8541 cnfcom2 8543 infxpenc 8785 infxpenc2 8789 pwfseqlem5 9429 pwfseq 9430 summolem3 14378 summo 14381 fsum 14384 fsumf1o 14387 sumsn 14405 prodmolem3 14588 prodmo 14591 fprod 14596 fprodf1o 14601 prodsn 14617 prodsnf 14619 gsumvalx 17191 gsumpropd 17193 gsumpropd2lem 17194 gsumval3lem1 18227 gsumval3 18229 znhash 19826 znunithash 19832 imasf1oxms 22204 cncfcnvcn 22632 wlksnwwlknvbij 26672 clwwlksvbij 26788 eupthp1 26942 f1ocnt 29400 derangval 30857 subfacp1lem2a 30870 subfacp1lem3 30872 subfacp1lem5 30874 erdsze2lem1 30893 ismtyval 33231 rngoisoval 33408 lautset 34848 pautsetN 34864 eldioph2lem1 36803 imasgim 37150 sumsnd 38668 f1oeq2d 38835 sumsnf 39205 stoweidlem35 39559 stoweidlem39 39563 uspgrsprfo 41044