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 6838

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 6801	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–1-1→𝐴 ↔ 𝐹:𝐶–1-1→𝐵))
2		foeq3 6818	. . 3 ⊢ (𝐴 = 𝐵 → (𝐹:𝐶–onto→𝐴 ↔ 𝐹:𝐶–onto→𝐵))
3	1, 2	anbi12d 632	. 2 ⊢ (𝐴 = 𝐵 → ((𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴) ↔ (𝐹:𝐶–1-1→𝐵 ∧ 𝐹:𝐶–onto→𝐵)))
4		df-f1o 6569	. 2 ⊢ (𝐹:𝐶–1-1-onto→𝐴 ↔ (𝐹:𝐶–1-1→𝐴 ∧ 𝐹:𝐶–onto→𝐴))
5		df-f1o 6569	. 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 1536 –1-1→wf1 6559 –onto→wfo 6560 –1-1-onto→wf1o 6561

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-9 2115 ax-ext 2705

This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1776 df-cleq 2726 df-ss 3979 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569

This theorem is referenced by: f1oeq23 6839 f1oeq123d 6842 f1oeq3d 6845 f1ores 6862 resin 6870 isoeq5 7340 breng 8992 xpcomf1o 9099 isinf 9293 isinfOLD 9294 cnfcom2 9739 fin1a2lem6 10442 pwfseqlem5 10700 pwfseq 10701 hashgf1o 14008 axdc4uzlem 14020 sumeq1 15721 prodeq1f 15938 prodeq1 15939 prodeq1i 15948 unbenlem 16941 4sqlem11 16988 gsumvalx 18701 cayley 19446 cayleyth 19447 ovolicc2lem4 25568 logf1o2 26706 uspgrf1oedg 29204 uspgredgiedg 29206 wlkiswwlks2lem4 29901 clwwlknonclwlknonf1o 30390 dlwwlknondlwlknonf1o 30393 adjbd1o 32113 rinvf1o 32646 cshf1o 32931 eulerpartgbij 34353 eulerpartlemgh 34359 derangval 35151 subfacp1lem2a 35164 subfacp1lem3 35166 subfacp1lem5 35168 mrsubff1o 35499 msubff1o 35541 cbvprodvw2 36229 bj-finsumval0 37267 f1omptsnlem 37318 f1omptsn 37319 poimirlem9 37615 poimirlem15 37621 ismtyval 37786 ismrer1 37824 lautset 40064 pautsetN 40080 hvmap1o2 41747 pwfi2f1o 43084 imasgim 43088 alephiso2 43547 f1ocof1ob2 47031 isuspgrim0lem 47808 gricushgr 47823 grtriprop 47845 grtrif1o 47846 isgrtri 47847 uspgrsprfo 47991