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 6754

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 6717	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6734	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6489	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6489	. 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 1540 –1-1→wf1 6479 –onto→wfo 6480 –1-1-onto→wf1o 6481

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-9 2119 ax-ext 2701

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2721 df-ss 3920 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489

This theorem is referenced by: f1oeq23 6755 f1oeq123d 6758 f1oeq3d 6761 f1ores 6778 resin 6786 isoeq5 7258 breng 8881 xpcomf1o 8983 isinf 9154 cnfcom2 9598 fin1a2lem6 10299 pwfseqlem5 10557 pwfseq 10558 hashgf1o 13878 axdc4uzlem 13890 sumeq1 15596 prodeq1f 15813 prodeq1 15814 prodeq1i 15823 unbenlem 16820 4sqlem11 16867 gsumvalx 18550 cayley 19293 cayleyth 19294 ovolicc2lem4 25419 logf1o2 26557 uspgrf1oedg 29118 uspgredgiedg 29120 wlkiswwlks2lem4 29817 clwwlknonclwlknonf1o 30306 dlwwlknondlwlknonf1o 30309 adjbd1o 32029 rinvf1o 32574 cshf1o 32905 eulerpartgbij 34346 eulerpartlemgh 34352 derangval 35150 subfacp1lem2a 35163 subfacp1lem3 35165 subfacp1lem5 35167 mrsubff1o 35498 msubff1o 35540 cbvprodvw2 36231 bj-finsumval0 37269 f1omptsnlem 37320 f1omptsn 37321 poimirlem9 37619 poimirlem15 37625 ismtyval 37790 ismrer1 37828 lautset 40071 pautsetN 40087 hvmap1o2 41754 pwfi2f1o 43079 imasgim 43083 alephiso2 43541 f1ocof1ob2 47076 isuspgrim0lem 47887 gricushgr 47911 grtriprop 47935 grtrif1o 47936 isgrtri 47937 uspgrsprfo 48142