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 6766

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 6729	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6746	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 633	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6501	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6501	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐵 ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵))
6	3, 4, 5	3bitr4g 314	1 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:𝐶–1-1-onto→𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 –1-1→wf1 6491 –onto→wfo 6492 –1-1-onto→wf1o 6493

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-9 2124 ax-ext 2709

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1782 df-cleq 2729 df-ss 3907 df-f 6498 df-f1 6499 df-fo 6500 df-f1o 6501

This theorem is referenced by: f1oeq23 6767 f1oeq123d 6770 f1oeq3d 6773 f1ores 6790 resin 6798 isoeq5 7271 breng 8897 xpcomf1o 8999 isinf 9170 cnfcom2 9618 fin1a2lem6 10322 pwfseqlem5 10581 pwfseq 10582 hashgf1o 13928 axdc4uzlem 13940 sumeq1 15646 prodeq1f 15866 prodeq1 15867 prodeq1i 15876 unbenlem 16874 4sqlem11 16921 gsumvalx 18639 cayley 19384 cayleyth 19385 ovolicc2lem4 25501 logf1o2 26631 uspgrf1oedg 29260 uspgredgiedg 29262 wlkiswwlks2lem4 29959 clwwlknonclwlknonf1o 30451 dlwwlknondlwlknonf1o 30454 adjbd1o 32175 rinvf1o 32722 cshf1o 33041 eulerpartgbij 34536 eulerpartlemgh 34542 derangval 35369 subfacp1lem2a 35382 subfacp1lem3 35384 subfacp1lem5 35386 mrsubff1o 35717 msubff1o 35759 cbvprodvw2 36449 bj-finsumval0 37619 f1omptsnlem 37670 f1omptsn 37671 poimirlem9 37968 poimirlem15 37974 ismtyval 38139 ismrer1 38177 lautset 40546 pautsetN 40562 hvmap1o2 42229 pwfi2f1o 43546 imasgim 43550 alephiso2 44007 f1ocof1ob2 47546 isuspgrim0lem 48385 gricushgr 48409 grtriprop 48433 grtrif1o 48434 isgrtri 48435 uspgrsprfo 48640