f1oeq3 - Metamath Proof Explorer

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

Theorem f1oeq3 6629

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

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

**Proof of Theorem f1oeq3**
Step	Hyp	Ref	Expression
1		f1eq3 6590	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6609	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 634	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6365	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6365	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 317	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 = wceq 1543 –1-1→wf1 6355 –onto→wfo 6356 –1-1-onto→wf1o 6357

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708

This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-v 3400 df-in 3860 df-ss 3870 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365

This theorem is referenced by: f1oeq23 6630 f1oeq123d 6633 f1oeq3d 6636 f1ores 6653 resin 6660 isoeq5 7108 breng 8613 brenOLD 8615 xpcomf1o 8712 isinf 8867 cnfcom2 9295 fin1a2lem6 9984 pwfseqlem5 10242 pwfseq 10243 hashgf1o 13509 axdc4uzlem 13521 sumeq1 15217 prodeq1f 15433 unbenlem 16424 4sqlem11 16471 gsumvalx 18102 cayley 18760 cayleyth 18761 ovolicc2lem4 24371 logf1o2 25492 uspgrf1oedg 27218 wlkiswwlks2lem4 27910 clwwlknonclwlknonf1o 28399 dlwwlknondlwlknonf1o 28402 adjbd1o 30120 rinvf1o 30638 cshf1o 30908 eulerpartgbij 32005 eulerpartlemgh 32011 derangval 32796 subfacp1lem2a 32809 subfacp1lem3 32811 subfacp1lem5 32813 mrsubff1o 33144 msubff1o 33186 bj-finsumval0 35140 f1omptsnlem 35193 f1omptsn 35194 poimirlem9 35472 poimirlem15 35478 ismtyval 35644 ismrer1 35682 lautset 37782 pautsetN 37798 hvmap1o2 39465 pwfi2f1o 40565 imasgim 40569 alephiso2 40782 f1ocof1ob2 44189 isomushgr 44894 uspgrsprfo 44926